MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpd3an3 Structured version   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  6291  f1oeng  7126  wdomimag  7555  cdaval  8050  gruuni  8675  genpv  8876  infmssuzle  10558  fzrevral3  11133  subsq2  11489  brfi1ind  11716  caubnd  12162  dvdsmul1  12871  dvdsmul2  12872  hashbcval  13370  setsvalg  13492  ressval  13516  restval  13654  latjle12  14491  latlem12  14507  lublem  14545  clatglb  14551  mrelatglb0  14611  imasmnd2  14732  divsinv  14999  ghminv  15013  symgov  15100  gexod  15220  lsmvalx  15273  rngrz  15701  imasrng  15725  irredneg  15815  ocvin  16901  restin  17230  qtopval  17727  elqtop3  17735  elfm3  17982  flimval  17995  nmge0  18663  nmeq0  18664  nminv  18667  nmo0  18769  0nghm  18775  evlrhm  19946  coemulhi  20172  isosctrlem2  20663  divsqrsumlem  20818  elghomlem1  21949  rngorz  21990  nvge0  22163  nvnd  22180  dip0r  22216  dip0l  22217  nmoo0  22292  hi2eq  22607  unitdivcld  24299  ltflcei  26239  lxflflp1  26241  rngonegmn1l  26565  rngonegmn1r  26566  igenval  26671  pellfund14  26961  mendmulr  27473  fmuldfeq  27689  stoweidlem19  27744  stoweidlem26  27751  swrdrlen  28184  addlenrevswrd  28185  cshwlen  28241  lfl0  29863  op0le  29984  ople1  29989  olj01  30023  olm11  30025  atl0le  30102  hl2at  30202  pmapeq0  30563  trlcl  30961  trlle  30981  tendoid  31570  tendo0plr  31589  tendoipl2  31595  erngmul  31603  erngmul-rN  31611  dvamulr  31809  dvavadd  31812  dvhmulr  31884  cdlemm10N  31916
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