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 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 519 . 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 366    /\ wa 367
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 368  df-an 369
This theorem is referenced by:  anddi  868  cases  968  cador  1465  rexun  3598  rabun2  3702  reuun2  3706  xpundir  4967  coundi  5416  mptun  5620  tpostpos  6893  wemapsolem  7890  ltxr  11245  hashbclem  12405  hashf1lem2  12409  pythagtriplem2  14343  pythagtrip  14360  vdwapun  14494  legtrid  24098  colinearalg  24334  usgraedg4  24508  vdgrun  25022  vdgrfiun  25023  elimifd  27546  dfon2lem5  29384  nobndup  29625  nofulllem5  29631  seglelin  29919  cnambfre  30228  expdioph  31131  usgvincvad  32722  usgvincvadALT  32725  rp-isfinite6  38173
  Copyright terms: Public domain W3C validator