Theorem andi | index | src |

theorem andi (a b c: wff): $ a /\ (b \/ c) <-> a /\ b \/ a /\ c $;
StepHypRefExpression
1 ian
a -> b -> a /\ b
2 ian
a -> c -> a /\ c
3 1, 2 orimd
a -> b \/ c -> a /\ b \/ a /\ c
4 3 imp
a /\ (b \/ c) -> a /\ b \/ a /\ c
5 eor
(a /\ b -> a /\ (b \/ c)) -> (a /\ c -> a /\ (b \/ c)) -> a /\ b \/ a /\ c -> a /\ (b \/ c)
6 anim2
(b -> b \/ c) -> a /\ b -> a /\ (b \/ c)
7 orl
b -> b \/ c
8 6, 7 ax_mp
a /\ b -> a /\ (b \/ c)
9 5, 8 ax_mp
(a /\ c -> a /\ (b \/ c)) -> a /\ b \/ a /\ c -> a /\ (b \/ c)
10 anim2
(c -> b \/ c) -> a /\ c -> a /\ (b \/ c)
11 orr
c -> b \/ c
12 10, 11 ax_mp
a /\ c -> a /\ (b \/ c)
13 9, 12 ax_mp
a /\ b \/ a /\ c -> a /\ (b \/ c)
14 4, 13 ibii
a /\ (b \/ c) <-> a /\ b \/ a /\ c

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp)