theorem bian1exd (G b: wff) {x: nat} (a c: wff x): $ G -> (a <-> b /\ c) $ > $ G -> (E. x a <-> b /\ E. x c) $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | exan1 | E. x (b /\ c) <-> b /\ E. x c |
|
2 | hyp h | G -> (a <-> b /\ c) |
|
3 | 2 | exeqd | G -> (E. x a <-> E. x (b /\ c)) |
4 | 1, 3 | syl6bb | G -> (E. x a <-> b /\ E. x c) |