theorem aneq1da (G a b c: wff): $ G /\ c -> (a <-> b) $ > $ G -> (a /\ c <-> b /\ c) $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | aneq1a | (c -> (a <-> b)) -> (a /\ c <-> b /\ c) |
|
2 | hyp h | G /\ c -> (a <-> b) |
|
3 | 2 | exp | G -> c -> (a <-> b) |
4 | 1, 3 | syl | G -> (a /\ c <-> b /\ c) |