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

Theorem andir 858
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 857 . 2  |-  ( ( ch  /\  ( ph  \/  ps ) )  <->  ( ( ch  /\  ph )  \/  ( ch  /\  ps ) ) )
2 ancom 448 . 2  |-  ( ( ( ph  \/  ps )  /\  ch )  <->  ( ch  /\  ( ph  \/  ps ) ) )
3 ancom 448 . . 3  |-  ( (
ph  /\  ch )  <->  ( ch  /\  ph )
)
4 ancom 448 . . 3  |-  ( ( ps  /\  ch )  <->  ( ch  /\  ps )
)
53, 4orbi12i 518 . 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  860  jaoi2OLD  955  cases  957  cador  1437  rexun  3533  rabun2  3626  reuun2  3630  xpundir  4888  coundi  5336  mptun  5538  tpostpos  6764  wemapsolem  7760  ltxr  11091  hashbclem  12201  hashf1lem2  12205  pythagtriplem2  13880  pythagtrip  13897  vdwapun  14031  legtrid  22977  colinearalg  23091  usgraedg4  23240  vdgrun  23506  vdgrfiun  23507  elimifd  25840  elim2if  25841  dfon2lem5  27529  nobndup  27770  nofulllem5  27776  seglelin  28076  cnambfre  28365  expdioph  29297
  Copyright terms: Public domain W3C validator