Theorem andir 831

Description: Distributive law for conjunction. (Contributed by NM, 12-Aug-1994.)

Assertion

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

Proof of Theorem andir

Step	Hyp	Ref	Expression
1		andi 830	. 2 |- ( ( ch /\ ( ph \/ ps ) ) <-> ( ( ch /\ ph ) \/ ( ch /\ ps ) ) )
2		ancom 266	. 2 |- ( ( ( ph \/ ps ) /\ ch ) <-> ( ch /\ ( ph \/ ps ) ) )
3		ancom 266	. . 3 |- ( ( ph /\ ch ) <-> ( ch /\ ph ) )
4		ancom 266	. . 3 |- ( ( ps /\ ch ) <-> ( ch /\ ps ) )
5	3, 4	orbi12i 776	. 2 |- ( ( ( ph /\ ch ) \/ ( ps /\ ch ) ) <-> ( ( ch /\ ph ) \/ ( ch /\ ps ) ) )
6	1, 2, 5	3bitr4i 212	1 |- ( ( ( ph \/ ps ) /\ ch ) <-> ( ( ph /\ ch ) \/ ( ps /\ ch ) ) )

This proof depends on syntax axioms:   /\ wa 104   <-> wb 105   \/ wo 720

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721

This proof depends on definitions:  df-bi 117

This theorem is used by:  anddi  833  excxor  1427  xordc1  1442  sbequilem  1891  rexun  3409  rabun2  3512  reuun2  3516  xpundir  4830  coundi  5287  mptun  5513  tpostpos  6529  ltxr  10160  hashfibclem  11265  hashf1lem2  11269  pythagtriplem2  13028  pythagtrip  13045  vtxdfifiun  16521