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

Theorem andir 866
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 865 . 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  868  jaoi2OLD  967  cases  969  cador  1442  rexun  3684  rabun2  3777  reuun2  3781  xpundir  5052  coundi  5507  mptun  5711  tpostpos  6975  wemapsolem  7974  ltxr  11323  hashbclem  12466  hashf1lem2  12470  pythagtriplem2  14199  pythagtrip  14216  vdwapun  14350  legtrid  23721  colinearalg  23905  usgraedg4  24079  vdgrun  24593  vdgrfiun  24594  elimifd  27111  elim2if  27112  dfon2lem5  28812  nobndup  29053  nofulllem5  29059  seglelin  29359  cnambfre  29656  expdioph  30585  usgvincvad  31887  usgvincvadALT  31890
  Copyright terms: Public domain W3C validator