Theorem andir 863

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 862	. 2 |- ( ( ch /\ ( ph \/ ps ) ) <-> ( ( ch /\ ph ) \/ ( ch /\ ps ) ) )
2		ancom 450	. 2 |- ( ( ( ph \/ ps ) /\ ch ) <-> ( ch /\ ( ph \/ ps ) ) )
3		ancom 450	. . 3 |- ( ( ph /\ ch ) <-> ( ch /\ ph ) )
4		ancom 450	. . 3 |- ( ( ps /\ ch ) <-> ( ch /\ ps ) )
5	3, 4	orbi12i 521	. 2 |- ( ( ( ph /\ ch ) \/ ( ps /\ ch ) ) <-> ( ( ch /\ ph ) \/ ( ch /\ ps ) ) )
6	1, 2, 5	3bitr4i 277	1 |- ( ( ( ph \/ ps ) /\ ch ) <-> ( ( ph /\ ch ) \/ ( ps /\ ch ) ) )

Syntax hints:   <-> wb 184   \/ wo 368   /\ wa 369

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371

This theorem is referenced by:  anddi  865  jaoi2OLD  960  cases  962  cador  1432  rexun  3536  rabun2  3629  reuun2  3633  xpundir  4892  coundi  5339  mptun  5541  tpostpos  6765  wemapsolem  7764  ltxr  11095  hashbclem  12205  hashf1lem2  12209  pythagtriplem2  13884  pythagtrip  13901  vdwapun  14035  legtrid  23022  colinearalg  23156  usgraedg4  23305  vdgrun  23571  vdgrfiun  23572  elimifd  25905  elim2if  25906  dfon2lem5  27600  nobndup  27841  nofulllem5  27847  seglelin  28147  cnambfre  28440  expdioph  29372