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  6080  f1oeng  6896  wdomimag  7317  cdaval  7812  gruuni  8438  genpv  8639  infmssuzle  10316  fzrevral3  10884  subsq2  11227  caubnd  11858  dvdsmul1  12566  dvdsmul2  12567  hashbcval  13065  setsvalg  13187  ressval  13211  restval  13347  latjle12  14184  latlem12  14200  lublem  14238  clatglb  14244  mrelatglb0  14304  imasmnd2  14425  divsinv  14692  ghminv  14706  symgov  14793  gexod  14913  lsmvalx  14966  rngrz  15394  imasrng  15418  irredneg  15508  ocvin  16590  restin  16913  qtopval  17402  elqtop3  17410  elfm3  17661  flimval  17674  nmge0  18154  nmeq0  18155  nminv  18158  nmo0  18260  0nghm  18266  evlrhm  19425  coemulhi  19651  isosctrlem2  20135  divsqrsumlem  20290  elghomlem1  21044  rngorz  21085  nvge0  21256  nvnd  21273  dip0r  21309  dip0l  21310  nmoo0  21385  hi2eq  21700  unitdivcld  23300  ltflcei  24998  lxflflp1  25000  ov2gc  25226  ov4gc  25227  caytr  25503  addidrv2  25761  valtar  25986  rngonegmn1l  26683  rngonegmn1r  26684  igenval  26789  pellfund14  27086  mendmulr  27599  stoweidlem26  27878  lfl0  29877  op0le  29998  ople1  30003  olj01  30037  olm11  30039  atl0le  30116  hl2at  30216  pmapeq0  30577  trlcl  30975  trlle  30995  tendoid  31584  tendo0plr  31603  tendoipl2  31609  erngmul  31617  erngmul-rN  31625  dvamulr  31823  dvavadd  31826  dvhmulr  31898  cdlemm10N  31930
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