theorem aneqd (a b c d e: wff): $ a -> (b <-> c) $ > $ a -> (d <-> e) $ > $ a -> (b /\ d <-> c /\ e) $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hyp h1 | a -> (b <-> c) |
|
2 | 1 | bi1d | a -> b -> c |
3 | hyp h2 | a -> (d <-> e) |
|
4 | 3 | bi1d | a -> d -> e |
5 | 2, 4 | animd | a -> b /\ d -> c /\ e |
6 | 1 | bi2d | a -> c -> b |
7 | 3 | bi2d | a -> e -> d |
8 | 6, 7 | animd | a -> c /\ e -> b /\ d |
9 | 5, 8 | ibid | a -> (b /\ d <-> c /\ e) |