theorem birexan2i (a: wff) {x: nat} (p b c: wff x): $ b <-> E. x (p /\ c) $ > $ a /\ b <-> E. x (p /\ (a /\ c)) $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hyp h | b <-> E. x (p /\ c) |
|
2 | 1 | a1i | a -> (b <-> E. x (p /\ c)) |
3 | 2 | birexan2a | a /\ b <-> E. x (p /\ (a /\ c)) |