theorem biexexi {x y: nat} (a b: wff x y): $ a <-> E. y b $ > $ E. x a <-> E. y E. x b $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bitr4 | (E. x a <-> E. x E. y b) -> (E. y E. x b <-> E. x E. y b) -> (E. x a <-> E. y E. x b) |
|
2 | hyp h | a <-> E. y b |
|
3 | 2 | exeqi | E. x a <-> E. x E. y b |
4 | 1, 3 | ax_mp | (E. y E. x b <-> E. x E. y b) -> (E. x a <-> E. y E. x b) |
5 | excomb | E. y E. x b <-> E. x E. y b |
|
6 | 4, 5 | ax_mp | E. x a <-> E. y E. x b |