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

Theorem mpd3an3 1278
Description: An inference based on modus ponens. (Contributed by NM, 8-Nov-2007.)
Hypotheses
Ref Expression
mpd3an3.2  |-  ( (
ph  /\  ps )  ->  ch )
mpd3an3.3  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Assertion
Ref Expression
mpd3an3  |-  ( (
ph  /\  ps )  ->  th )

Proof of Theorem mpd3an3
StepHypRef Expression
1 mpd3an3.2 . 2  |-  ( (
ph  /\  ps )  ->  ch )
2 mpd3an3.3 . . 3  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
323expa 1151 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
41, 3mpdan 649 1  |-  ( (
ph  /\  ps )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  elovmpt2  6066  f1oeng  6882  wdomimag  7303  cdaval  7798  gruuni  8424  genpv  8625  infmssuzle  10302  fzrevral3  10870  subsq2  11213  caubnd  11844  dvdsmul1  12552  dvdsmul2  12553  hashbcval  13051  setsvalg  13173  ressval  13197  restval  13333  latjle12  14170  latlem12  14186  lublem  14224  clatglb  14230  mrelatglb0  14290  imasmnd2  14411  divsinv  14678  ghminv  14692  symgov  14779  gexod  14899  lsmvalx  14952  rngrz  15380  imasrng  15404  irredneg  15494  ocvin  16576  restin  16899  qtopval  17388  elqtop3  17396  elfm3  17647  flimval  17660  nmge0  18140  nmeq0  18141  nminv  18144  nmo0  18246  0nghm  18252  evlrhm  19411  coemulhi  19637  isosctrlem2  20121  divsqrsumlem  20276  elghomlem1  21030  rngorz  21071  nvge0  21242  nvnd  21259  dip0r  21295  dip0l  21296  nmoo0  21371  hi2eq  21686  unitdivcld  23287  ltflcei  24930  lxflflp1  24932  ov2gc  25134  ov4gc  25135  caytr  25411  addidrv2  25669  valtar  25894  rngonegmn1l  26591  rngonegmn1r  26592  igenval  26697  pellfund14  26994  mendmulr  27507  stoweidlem26  27786  lfl0  29328  op0le  29449  ople1  29454  olj01  29488  olm11  29490  atl0le  29567  hl2at  29667  pmapeq0  30028  trlcl  30426  trlle  30446  tendoid  31035  tendo0plr  31054  tendoipl2  31060  erngmul  31068  erngmul-rN  31076  dvamulr  31274  dvavadd  31277  dvhmulr  31349  cdlemm10N  31381
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  df-3an 936
  Copyright terms: Public domain W3C validator