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

Theorem andi 838
Description: Distributive law for conjunction. Theorem *4.4 of [WhiteheadRussell] p. 118. (Contributed by NM, 5-Aug-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 375 . . 3  |-  ( (
ph  /\  ps )  ->  ( ( ph  /\  ps )  \/  ( ph  /\  ch ) ) )
2 olc 374 . . 3  |-  ( (
ph  /\  ch )  ->  ( ( ph  /\  ps )  \/  ( ph  /\  ch ) ) )
31, 2jaodan 761 . 2  |-  ( (
ph  /\  ( ps  \/  ch ) )  -> 
( ( ph  /\  ps )  \/  ( ph  /\  ch ) ) )
4 orc 375 . . . 4  |-  ( ps 
->  ( ps  \/  ch ) )
54anim2i 553 . . 3  |-  ( (
ph  /\  ps )  ->  ( ph  /\  ( ps  \/  ch ) ) )
6 olc 374 . . . 4  |-  ( ch 
->  ( ps  \/  ch ) )
76anim2i 553 . . 3  |-  ( (
ph  /\  ch )  ->  ( ph  /\  ( ps  \/  ch ) ) )
85, 7jaoi 369 . 2  |-  ( ( ( ph  /\  ps )  \/  ( ph  /\ 
ch ) )  -> 
( ph  /\  ( ps  \/  ch ) ) )
93, 8impbii 181 1  |-  ( (
ph  /\  ( ps  \/  ch ) )  <->  ( ( ph  /\  ps )  \/  ( ph  /\  ch ) ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    \/ wo 358    /\ wa 359
This theorem is referenced by:  andir  839  anddi  841  indi  3579  indifdir  3589  unrab  3604  unipr  4021  uniun  4026  unopab  4276  ordnbtwn  4663  xpundi  4921  coundir  5363  imadif  5519  unpreima  5847  difxp  6371  tpostpos  6490  elznn0nn  10284  faclbnd4lem4  11575  opsrtoslem1  16532  mbfmax  19529  fta1glem2  20077  ofmulrt  20187  lgsquadlem3  21128  ballotlemodife  24743  subfacp1lem6  24859  soseq  25509  lineunray  26029  itg2addnclem2  26203  lzunuz  26763  diophun  26769  rmydioph  27022
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 178  df-or 360  df-an 361
  Copyright terms: Public domain W3C validator