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