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

Theorem imdistani 671
Description: Distribution of implication with conjunction. (Contributed by NM, 1-Aug-1994.)
Hypothesis
Ref Expression
imdistani.1  |-  ( ph  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
imdistani  |-  ( (
ph  /\  ps )  ->  ( ph  /\  ch ) )

Proof of Theorem imdistani
StepHypRef Expression
1 imdistani.1 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
21anc2li 540 . 2  |-  ( ph  ->  ( ps  ->  ( ph  /\  ch ) ) )
32imp 418 1  |-  ( (
ph  /\  ps )  ->  ( ph  /\  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  nfan1  1822  2eu1  2223  difrab  3442  onint  4586  foconst  5462  dffo4  5676  dffo5  5677  isofrlem  5837  tz7.48lem  6453  opthreg  7319  axpowndlem3  8221  eltsk2g  8373  recgt1i  9653  sup2  9710  elnnnn0c  10009  elnnz1  10049  recnz  10087  eluz2b2  10290  iccsplit  10768  elfzp12  10861  1mod  10996  cos01gt0  12471  clatl  14220  isacs4lem  14271  isacs5lem  14272  elply2  19578  3oalem1  22241  ballotlemfc0  23051  ballotlemfcc  23052  ballotlemodife  23056  ballotth  23096  measvunilem  23540  probun  23622  elorrvc  23664  areacirclem6  24930  tolat  25286  ablocomgrp  25342  setiscat  25979  opnrebl2  26236  syldanl  26334  seqpo  26457  incsequz  26458  incsequz2  26459  ismtycnv  26526  prnc  26692  climsuselem1  27733  climsuse  27734  ioovolcl  27742  stirlinglem11  27833  2reu1  27964  dihatexv2  31529
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-an 360
  Copyright terms: Public domain W3C validator