theorem iexe {x: nat} (a: nat) (b: wff x) (c: wff): $ x = a -> (b <-> c) $ > $ c -> E. x b $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hyp e | x = a -> (b <-> c) |
|
2 | 1 | anwr | c /\ x = a -> (b <-> c) |
3 | anl | c /\ x = a -> c |
|
4 | 2, 3 | mpbird | c /\ x = a -> b |
5 | 4 | iexde | c -> E. x b |