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

Theorem andir 884
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 883 . 2  |-  ( ( ch  /\  ( ph  \/  ps ) )  <->  ( ( ch  /\  ph )  \/  ( ch  /\  ps ) ) )
2 ancom 456 . 2  |-  ( ( ( ph  \/  ps )  /\  ch )  <->  ( ch  /\  ( ph  \/  ps ) ) )
3 ancom 456 . . 3  |-  ( (
ph  /\  ch )  <->  ( ch  /\  ph )
)
4 ancom 456 . . 3  |-  ( ( ps  /\  ch )  <->  ( ch  /\  ps )
)
53, 4orbi12i 528 . 2  |-  ( ( ( ph  /\  ch )  \/  ( ps  /\ 
ch ) )  <->  ( ( ch  /\  ph )  \/  ( ch  /\  ps ) ) )
61, 2, 53bitr4i 285 1  |-  ( ( ( ph  \/  ps )  /\  ch )  <->  ( ( ph  /\  ch )  \/  ( ps  /\  ch ) ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 189    \/ wo 374    /\ wa 375
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 190  df-or 376  df-an 377
This theorem is referenced by:  anddi  886  cases  988  cador  1522  rexun  3626  rabun2  3734  reuun2  3738  xpundir  4907  coundi  5355  mptun  5731  tpostpos  7019  wemapsolem  8091  ltxr  11444  hashbclem  12648  hashf1lem2  12652  pythagtriplem2  14816  pythagtrip  14833  vdwapun  14973  legtrid  24685  colinearalg  24989  usgraedg4  25163  vdgrun  25678  vdgrfiun  25679  elimifd  28209  dfon2lem5  30482  nobndup  30638  nofulllem5  30644  seglelin  30932  poimirlem30  32015  poimirlem31  32016  cnambfre  32034  expdioph  35923  rp-isfinite6  36208  vtxduhgrun  39588  usgvincvad  39989  usgvincvadALT  39992
  Copyright terms: Public domain W3C validator