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  3188  0disj  4016  disjx0  4018  relres  4983  cnvdif  5087  funopab4  5289  fun0  5307  fvsn  5713  difxp  6153  reltpos  6239  tpostpos  6254  tpos0  6264  oaabs2  6643  swoer  6688  xpider  6730  erinxp  6733  sbthcl  6983  php  7045  inf0  7322  unctb  7831  fin1a2lem12  8037  axcc2lem  8062  axcclem  8083  brdom3  8153  brdom5  8154  brdom4  8155  pwcfsdom  8205  smobeth  8208  fpwwe2lem8  8259  fpwwe2lem9  8260  fpwwe2lem12  8263  pwxpndom2  8287  pwcdandom  8289  gchac  8295  wunex3  8363  inar1  8397  gruina  8440  ltsopi  8512  recmulnq  8588  prcdnq  8617  ltrel  8887  lerel  8889  cnexALT  10350  dfle2  10481  dflt2  10482  uzrdg0i  11022  ltwefz  11026  fzennn  11030  faclbnd4lem1  11306  hashsslei  11378  isercolllem1  12138  zsum  12191  sum0  12194  xpnnenOLD  12488  znnen  12491  qnnen  12492  rpnnen  12505  ruc  12521  nthruc  12529  nthruz  12530  phicl2  12836  pwsle  13391  xpsc0  13462  xpsc1  13463  relfull  13782  relfth  13783  gicer  14740  oppglsm  14953  efgrelexlemb  15059  isunit  15439  opsrtoslem2  16226  pjpm  16608  1stcfb  17171  2ndc1stc  17177  2ndcctbss  17181  2ndcdisj2  17183  2ndcsep  17185  hmpher  17475  met1stc  18067  re2ndc  18307  iccpnfhmeo  18443  xrhmeo  18444  xrcmp  18446  xrcon  18447  dyadmbl  18955  opnmblALT  18958  vitalilem2  18964  vitalilem3  18965  vitali  18968  mbfimaopnlem  19010  mbfsup  19019  dgrval  19610  dgrcl  19615  dgrub  19616  dgrlb  19618  aannenlem3  19710  dvrelog  19984  logcn  19994  logccv  20010  ppiub  20443  lgsquadlem1  20593  lgsquadlem2  20594  dirith2  20677  nvrel  21158  phrel  21393  bnrel  21446  hlrel  21469  pjnormi  22300  lnopunilem1  22590  lnophmlem1  22596  ssnnssfz  23277  xrge0iifiso  23317  erdszelem4  23725  erdszelem8  23729  konigsberg  23911  supfz  24094  inffz  24095  elrn3  24120  omsinds  24219  naim1i  24825  naim2i  24826  mont  24848  onpsstopbas  24869  wl-bitri  24911  domrancur1b  25200  dfps2  25289  prismorcsetlemc  25917  pgapspf  26052  trer  26227  fneer  26288  incsequz2  26459  cncfres  26485  heiborlem3  26537  rencldnfilem  26903  pellexlem4  26917  pellexlem5  26918  jm2.23  27089  ttac  27129  idomsubgmo  27514  lhe4.4ex1a  27546  itgsin0pilem1  27744  itgsinexplem1  27748  wallispilem2  27815  wallispilem4  27817  wallispi  27819  usgraexmpldifpr  28132  usgraexmpl  28133  onfrALTlem5  28307  e000  28542  e00  28543  bnj1023  28812  bnj1109  28818  diclspsn  31384  dih1dimatlem  31519
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator