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

Theorem imdistani 690
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 557 . 2  |-  ( ph  ->  ( ps  ->  ( ph  /\  ch ) ) )
32imp 429 1  |-  ( (
ph  /\  ps )  ->  ( ph  /\  ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ 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-an 371
This theorem is referenced by:  cases2  970  cases2OLD  971  nfan1  1874  2eu1OLD  2387  difrab  3772  rabsnifsb  4095  foconst  5805  elfvmptrab  5970  dffo4  6036  dffo5  6037  isofrlem  6223  onint  6609  tz7.48lem  7106  opthreg  8034  axpowndlem3OLD  8975  eltsk2g  9128  recgt1i  10441  sup2  10498  elnnnn0c  10840  elnnz1  10889  recnz  10935  eluz2b2  11153  iccsplit  11652  elfzp12  11756  1mod  11995  2swrd1eqwrdeq  12641  cos01gt0  13786  reumodprminv  14187  clatl  15602  isacs4lem  15654  isacs5lem  15655  isnzr2hash  17706  mplcoe5lem  17917  ioovolcl  21730  elply2  22344  wlkonprop  24227  trlonprop  24236  pthonprop  24271  spthonprp  24279  3oalem1  26272  elorrvc  28058  ballotlemfc0  28087  ballotlemfcc  28088  ballotlemodife  28092  ballotth  28132  wl-ax11-lem3  29620  mblfinlem1  29644  ovoliunnfl  29649  voliunnfl  29651  itg2addnclem2  29660  areacirclem5  29704  opnrebl2  29732  syldanl  29821  seqpo  29859  incsequz  29860  incsequz2  29861  ismtycnv  29917  prnc  30083  fperiodmullem  31096  climsuselem1  31165  climsuse  31166  0ellimcdiv  31207  cncfiooicclem1  31248  fperdvper  31264  iblsplit  31300  stirlinglem11  31400  2reu1  31674  dihatexv2  36145
  Copyright terms: Public domain W3C validator