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

Theorem mpd3an3 1280
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 1153 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
41, 3mpdan 650 1  |-  ( (
ph  /\  ps )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  elovmpt2  6250  f1oeng  7085  wdomimag  7511  cdaval  8006  gruuni  8631  genpv  8832  infmssuzle  10514  fzrevral3  11088  subsq2  11444  brfi1ind  11671  caubnd  12117  dvdsmul1  12826  dvdsmul2  12827  hashbcval  13325  setsvalg  13447  ressval  13471  restval  13609  latjle12  14446  latlem12  14462  lublem  14500  clatglb  14506  mrelatglb0  14566  imasmnd2  14687  divsinv  14954  ghminv  14968  symgov  15055  gexod  15175  lsmvalx  15228  rngrz  15656  imasrng  15680  irredneg  15770  ocvin  16856  restin  17184  qtopval  17680  elqtop3  17688  elfm3  17935  flimval  17948  nmge0  18616  nmeq0  18617  nminv  18620  nmo0  18722  0nghm  18728  evlrhm  19899  coemulhi  20125  isosctrlem2  20616  divsqrsumlem  20771  elghomlem1  21902  rngorz  21943  nvge0  22116  nvnd  22133  dip0r  22169  dip0l  22170  nmoo0  22245  hi2eq  22560  unitdivcld  24252  ltflcei  26140  lxflflp1  26142  rngonegmn1l  26455  rngonegmn1r  26456  igenval  26561  pellfund14  26851  mendmulr  27364  fmuldfeq  27580  stoweidlem19  27635  stoweidlem26  27642  swrdrlen  28003  addlenrevswrd  28004  lfl0  29548  op0le  29669  ople1  29674  olj01  29708  olm11  29710  atl0le  29787  hl2at  29887  pmapeq0  30248  trlcl  30646  trlle  30666  tendoid  31255  tendo0plr  31274  tendoipl2  31280  erngmul  31288  erngmul-rN  31296  dvamulr  31494  dvavadd  31497  dvhmulr  31569  cdlemm10N  31601
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-an 361  df-3an 938
  Copyright terms: Public domain W3C validator