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

Theorem mp2 17
Description: A double modus ponens inference. (Contributed by NM, 5-Apr-1994.) (Proof shortened by Wolf Lammen, 23-Jul-2013.)
Hypotheses
Ref Expression
mp2.1  |-  ph
mp2.2  |-  ps
mp2.3  |-  ( ph  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
mp2  |-  ch

Proof of Theorem mp2
StepHypRef Expression
1 mp2.1 . 2  |-  ph
2 mp2.2 . . 3  |-  ps
3 mp2.3 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
42, 3mpi 16 . 2  |-  ( ph  ->  ch )
51, 4ax-mp 8 1  |-  ch
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  impbii  180  pm3.2i  441  sstri  3201  0disj  4032  disjx0  4034  relres  4999  cnvdif  5103  funopab4  5305  fun0  5323  fvsn  5729  difxp  6169  reltpos  6255  tpostpos  6270  tpos0  6280  oaabs2  6659  swoer  6704  xpider  6746  erinxp  6749  sbthcl  6999  php  7061  inf0  7338  unctb  7847  fin1a2lem12  8053  axcc2lem  8078  axcclem  8099  brdom3  8169  brdom5  8170  brdom4  8171  pwcfsdom  8221  smobeth  8224  fpwwe2lem8  8275  fpwwe2lem9  8276  fpwwe2lem12  8279  pwxpndom2  8303  pwcdandom  8305  gchac  8311  wunex3  8379  inar1  8413  gruina  8456  ltsopi  8528  recmulnq  8604  prcdnq  8633  ltrel  8903  lerel  8905  cnexALT  10366  dfle2  10497  dflt2  10498  uzrdg0i  11038  ltwefz  11042  fzennn  11046  faclbnd4lem1  11322  hashsslei  11394  isercolllem1  12154  zsum  12207  sum0  12210  xpnnenOLD  12504  znnen  12507  qnnen  12508  rpnnen  12521  ruc  12537  nthruc  12545  nthruz  12546  phicl2  12852  pwsle  13407  xpsc0  13478  xpsc1  13479  relfull  13798  relfth  13799  gicer  14756  oppglsm  14969  efgrelexlemb  15075  isunit  15455  opsrtoslem2  16242  pjpm  16624  1stcfb  17187  2ndc1stc  17193  2ndcctbss  17197  2ndcdisj2  17199  2ndcsep  17201  hmpher  17491  met1stc  18083  re2ndc  18323  iccpnfhmeo  18459  xrhmeo  18460  xrcmp  18462  xrcon  18463  dyadmbl  18971  opnmblALT  18974  vitalilem2  18980  vitalilem3  18981  vitali  18984  mbfimaopnlem  19026  mbfsup  19035  dgrval  19626  dgrcl  19631  dgrub  19632  dgrlb  19634  aannenlem3  19726  dvrelog  20000  logcn  20010  logccv  20026  ppiub  20459  lgsquadlem1  20609  lgsquadlem2  20610  dirith2  20693  nvrel  21174  phrel  21409  bnrel  21462  hlrel  21485  pjnormi  22316  lnopunilem1  22606  lnophmlem1  22612  ssnnssfz  23292  xrge0iifiso  23332  erdszelem4  23740  erdszelem8  23744  konigsberg  23926  supfz  24109  inffz  24110  elrn3  24191  omsinds  24290  naim1i  24897  naim2i  24898  mont  24920  onpsstopbas  24941  wl-bitri  24983  domrancur1b  25303  dfps2  25392  prismorcsetlemc  26020  pgapspf  26155  trer  26330  fneer  26391  incsequz2  26562  cncfres  26588  heiborlem3  26640  rencldnfilem  27006  pellexlem4  27020  pellexlem5  27021  jm2.23  27192  ttac  27232  idomsubgmo  27617  lhe4.4ex1a  27649  itgsin0pilem1  27847  itgsinexplem1  27851  wallispilem2  27918  wallispilem4  27920  wallispi  27922  usgraexmpldifpr  28266  usgraexmpl  28267  onfrALTlem5  28606  e000  28856  e00  28857  bnj1023  29128  bnj1109  29134  diclspsn  32006  dih1dimatlem  32141
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator