theorem aneq1a (a b c: wff): $ (c -> (a <-> b)) -> (a /\ c <-> b /\ c) $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ancomb | a /\ c <-> c /\ a |
|
2 | ancomb | c /\ b <-> b /\ c |
|
3 | aneq2a | (c -> (a <-> b)) -> (c /\ a <-> c /\ b) |
|
4 | 2, 3 | syl6bb | (c -> (a <-> b)) -> (c /\ a <-> b /\ c) |
5 | 1, 4 | syl5bb | (c -> (a <-> b)) -> (a /\ c <-> b /\ c) |