MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  andir Structured version   Unicode version

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
StepHypRef 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 )
)
53, 4orbi12i 521 . 2  |-  ( ( ( ph  /\  ch )  \/  ( ps  /\ 
ch ) )  <->  ( ( ch  /\  ph )  \/  ( ch  /\  ps ) ) )
61, 2, 53bitr4i 277 1  |-  ( ( ( ph  \/  ps )  /\  ch )  <->  ( ( ph  /\  ch )  \/  ( ps  /\  ch ) ) )
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator