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  6064  f1oeng  6880  wdomimag  7301  cdaval  7796  gruuni  8422  genpv  8623  infmssuzle  10300  fzrevral3  10868  subsq2  11211  caubnd  11842  dvdsmul1  12550  dvdsmul2  12551  hashbcval  13049  setsvalg  13171  ressval  13195  restval  13331  latjle12  14168  latlem12  14184  lublem  14222  clatglb  14228  mrelatglb0  14288  imasmnd2  14409  divsinv  14676  ghminv  14690  symgov  14777  gexod  14897  lsmvalx  14950  rngrz  15378  imasrng  15402  irredneg  15492  ocvin  16574  restin  16897  qtopval  17386  elqtop3  17394  elfm3  17645  flimval  17658  nmge0  18138  nmeq0  18139  nminv  18142  nmo0  18244  0nghm  18250  evlrhm  19409  coemulhi  19635  isosctrlem2  20119  divsqrsumlem  20274  elghomlem1  21028  rngorz  21069  nvge0  21240  nvnd  21257  dip0r  21293  dip0l  21294  nmoo0  21369  hi2eq  21684  ov2gc  24535  ov4gc  24536  caytr  24812  addidrv2  25070  valtar  25295  rngonegmn1l  25992  rngonegmn1r  25993  igenval  26098  pellfund14  26395  mendmulr  26908  stoweidlem26  27187  lfl0  28628  op0le  28749  ople1  28754  olj01  28788  olm11  28790  atl0le  28867  hl2at  28967  pmapeq0  29328  trlcl  29726  trlle  29746  tendoid  30335  tendo0plr  30354  tendoipl2  30360  erngmul  30368  erngmul-rN  30376  dvamulr  30574  dvavadd  30577  dvhmulr  30649  cdlemm10N  30681
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