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

Theorem andi 862
Description: Distributive law for conjunction. Theorem *4.4 of [WhiteheadRussell] p. 118. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Wolf Lammen, 5-Jan-2013.)
Assertion
Ref Expression
andi  |-  ( (
ph  /\  ( ps  \/  ch ) )  <->  ( ( ph  /\  ps )  \/  ( ph  /\  ch ) ) )

Proof of Theorem andi
StepHypRef Expression
1 orc 385 . . 3  |-  ( (
ph  /\  ps )  ->  ( ( ph  /\  ps )  \/  ( ph  /\  ch ) ) )
2 olc 384 . . 3  |-  ( (
ph  /\  ch )  ->  ( ( ph  /\  ps )  \/  ( ph  /\  ch ) ) )
31, 2jaodan 783 . 2  |-  ( (
ph  /\  ( ps  \/  ch ) )  -> 
( ( ph  /\  ps )  \/  ( ph  /\  ch ) ) )
4 orc 385 . . . 4  |-  ( ps 
->  ( ps  \/  ch ) )
54anim2i 569 . . 3  |-  ( (
ph  /\  ps )  ->  ( ph  /\  ( ps  \/  ch ) ) )
6 olc 384 . . . 4  |-  ( ch 
->  ( ps  \/  ch ) )
76anim2i 569 . . 3  |-  ( (
ph  /\  ch )  ->  ( ph  /\  ( ps  \/  ch ) ) )
85, 7jaoi 379 . 2  |-  ( ( ( ph  /\  ps )  \/  ( ph  /\ 
ch ) )  -> 
( ph  /\  ( ps  \/  ch ) ) )
93, 8impbii 188 1  |-  ( (
ph  /\  ( ps  \/  ch ) )  <->  ( ( ph  /\  ps )  \/  ( ph  /\  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:  andir  863  anddi  865  cadan  1433  thema1a  1579  indi  3611  indifdir  3621  unrab  3636  unipr  4119  uniun  4125  unopab  4382  ordnbtwn  4824  xpundi  4906  difxp  5277  coundir  5355  imadif  5508  unpreima  5844  tpostpos  6780  elznn0nn  10675  faclbnd4lem4  12087  opsrtoslem1  17580  mbfmax  21142  fta1glem2  21653  ofmulrt  21763  lgsquadlem3  22710  ordtconlem1  26369  ballotlemodife  26895  subfacp1lem6  27088  soseq  27730  nobnddown  27857  lineunray  28193  itg2addnclem2  28463  lzunuz  29125  diophun  29131  rmydioph  29382
  Copyright terms: Public domain W3C validator