Theorem aneq2a | index | src |

theorem aneq2a (a b c: wff): $ (a -> (b <-> c)) -> (a /\ b <-> a /\ c) $;
StepHypRefExpression
1 anim2a
(a -> b -> c) -> a /\ b -> a /\ c
2 bi1
(b <-> c) -> b -> c
3 2 imim2i
(a -> (b <-> c)) -> a -> b -> c
4 1, 3 syl
(a -> (b <-> c)) -> a /\ b -> a /\ c
5 anim2a
(a -> c -> b) -> a /\ c -> a /\ b
6 bi2
(b <-> c) -> c -> b
7 6 imim2i
(a -> (b <-> c)) -> a -> c -> b
8 5, 7 syl
(a -> (b <-> c)) -> a /\ c -> a /\ b
9 4, 8 ibid
(a -> (b <-> c)) -> (a /\ b <-> a /\ c)

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp)