theorem rexal {x y: nat} (a: wff x) (b: wff x y):
$ E. x (a /\ A. y b) -> A. y E. x (a /\ b) $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | alan1 | A. y (a /\ b) <-> a /\ A. y b |
|
| 2 | 1 | exeqi | E. x A. y (a /\ b) <-> E. x (a /\ A. y b) |
| 3 | exal | E. x A. y (a /\ b) -> A. y E. x (a /\ b) |
|
| 4 | 2, 3 | sylbir | E. x (a /\ A. y b) -> A. y E. x (a /\ b) |