Theorem ordi 728

Description: Distributive law for disjunction. Theorem *4.41 of [WhiteheadRussell] p. 119. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 31-Jan-2015.)

Assertion

Ref	Expression
ordi	|- ((ph \/ (ps /\ ch)) <-> ((ph \/ ps) /\ (ph \/ ch)))

Proof of Theorem ordi

Step	Hyp	Ref	Expression
1		simpl 102	. . . 4 |- ((ps /\ ch) -> ps)
2	1	orim2i 677	. . 3 |- ((ph \/ (ps /\ ch)) -> (ph \/ ps))
3		simpr 103	. . . 4 |- ((ps /\ ch) -> ch)
4	3	orim2i 677	. . 3 |- ((ph \/ (ps /\ ch)) -> (ph \/ ch))
5	2, 4	jca 290	. 2 |- ((ph \/ (ps /\ ch)) -> ((ph \/ ps) /\ (ph \/ ch)))
6		orc 632	. . . 4 |- (ph -> (ph \/ (ps /\ ch)))
7	6	adantl 262	. . 3 |- (((ph \/ ps) /\ ph) -> (ph \/ (ps /\ ch)))
8	6	adantr 261	. . . 4 |- ((ph /\ ch) -> (ph \/ (ps /\ ch)))
9		olc 631	. . . 4 |- ((ps /\ ch) -> (ph \/ (ps /\ ch)))
10	8, 9	jaoian 708	. . 3 |- (((ph \/ ps) /\ ch) -> (ph \/ (ps /\ ch)))
11	7, 10	jaodan 709	. 2 |- (((ph \/ ps) /\ (ph \/ ch)) -> (ph \/ (ps /\ ch)))
12	5, 11	impbii 117	1 |- ((ph \/ (ps /\ ch)) <-> ((ph \/ ps) /\ (ph \/ ch)))

Syntax hints:   /\ wa 97   <-> wb 98   \/ wo 628

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  ordir  729  orddi  732  pm5.63dc  852  pm4.43  855  orbididc  859  undi  3179  undif4  3278  elnn1uz2  8320