theorem aleqdh {x: nat} (G a b: wff x): $ F/ x G $ > $ G -> (a <-> b) $ > $ G -> (A. x a <-> A. x b) $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | aleq | A. x (a <-> b) -> (A. x a <-> A. x b) |
|
2 | hyp h1 | F/ x G |
|
3 | hyp h | G -> (a <-> b) |
|
4 | 2, 3 | ialdh | G -> A. x (a <-> b) |
5 | 1, 4 | syl | G -> (A. x a <-> A. x b) |