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

Theorem andir 838
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 837 . 2  |-  ( ( ch  /\  ( ph  \/  ps ) )  <->  ( ( ch  /\  ph )  \/  ( ch  /\  ps ) ) )
2 ancom 437 . 2  |-  ( ( ( ph  \/  ps )  /\  ch )  <->  ( ch  /\  ( ph  \/  ps ) ) )
3 ancom 437 . . 3  |-  ( (
ph  /\  ch )  <->  ( ch  /\  ph )
)
4 ancom 437 . . 3  |-  ( ( ps  /\  ch )  <->  ( ch  /\  ps )
)
53, 4orbi12i 507 . 2  |-  ( ( ( ph  /\  ch )  \/  ( ps  /\ 
ch ) )  <->  ( ( ch  /\  ph )  \/  ( ch  /\  ps ) ) )
61, 2, 53bitr4i 268 1  |-  ( ( ( ph  \/  ps )  /\  ch )  <->  ( ( ph  /\  ch )  \/  ( ps  /\  ch ) ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    \/ wo 357    /\ wa 358
This theorem is referenced by:  anddi  840  cador  1381  rexun  3368  rabun2  3460  reuun2  3464  elimif  3607  xpundir  4758  coundi  5190  mptun  5390  tpostpos  6270  wemapso2lem  7281  ltxr  10473  hashbclem  11406  hashf1lem2  11410  pythagtriplem2  12886  pythagtrip  12903  vdwapun  13037  elimifd  23167  elim2if  23168  vdgrun  23908  dfon2lem5  24214  nobndup  24425  nofulllem5  24431  colinearalg  24610  seglelin  24811  anddi2  25044  vtarsuelt  25998  expdioph  27219  jaoi2  28176
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360
  Copyright terms: Public domain W3C validator