theorem rexeqa {x: nat} (p a b: wff x): $ p -> (a <-> b) $ > $ E. x (p /\ a) <-> E. x (p /\ b) $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | aneq2a | (p -> (a <-> b)) -> (p /\ a <-> p /\ b) |
|
2 | hyp h | p -> (a <-> b) |
|
3 | 1, 2 | ax_mp | p /\ a <-> p /\ b |
4 | 3 | exeqi | E. x (p /\ a) <-> E. x (p /\ b) |