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

Theorem mp2 9
Description: A double modus ponens inference. See mp2ALT 18 for a shorter proof using two more axioms. (Contributed by NM, 5-Apr-1994.) (Proof modification is discouraged.)
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.2 . 2  |-  ps
2 mp2.1 . . 3  |-  ph
3 mp2.3 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
42, 3ax-mp 8 . 2  |-  ( ps 
->  ch )
51, 4ax-mp 8 1  |-  ch
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  impbii  181  pm3.2i  442  sstri  3300  0disj  4146  disjx0  4148  relres  5114  cnvdif  5218  funopab4  5428  fun0  5448  fvsn  5865  difxp  6319  reltpos  6420  tpostpos  6435  tpos0  6445  oaabs2  6824  swoer  6869  xpider  6911  erinxp  6914  sbthcl  7165  php  7227  inf0  7509  unctb  8018  fin1a2lem12  8224  axcc2lem  8249  axcclem  8270  brdom3  8339  brdom5  8340  brdom4  8341  pwcfsdom  8391  smobeth  8394  fpwwe2lem8  8445  fpwwe2lem9  8446  fpwwe2lem12  8449  pwxpndom2  8473  pwcdandom  8475  gchac  8481  wunex3  8549  inar1  8583  gruina  8626  ltsopi  8698  recmulnq  8774  prcdnq  8803  ltrel  9073  lerel  9075  cnexALT  10540  dfle2  10672  dflt2  10673  uzrdg0i  11226  ltwefz  11230  fzennn  11234  faclbnd4lem1  11511  hashsslei  11612  isercolllem1  12385  zsum  12439  sum0  12442  xpnnenOLD  12736  znnen  12739  qnnen  12740  rpnnen  12753  ruc  12769  nthruc  12777  nthruz  12778  phicl2  13084  pwsle  13641  xpsc0  13712  xpsc1  13713  relfull  14032  relfth  14033  gicer  14990  oppglsm  15203  efgrelexlemb  15309  isunit  15689  opsrtoslem2  16472  pjpm  16858  1stcfb  17429  2ndc1stc  17435  2ndcctbss  17439  2ndcdisj2  17441  2ndcsep  17443  hmpher  17737  met1stc  18441  re2ndc  18703  iccpnfhmeo  18841  xrhmeo  18842  xrcmp  18844  xrcon  18845  dyadmbl  19359  opnmblALT  19362  vitalilem2  19368  vitalilem3  19369  vitali  19372  mbfimaopnlem  19414  mbfsup  19423  dgrval  20014  dgrcl  20019  dgrub  20020  dgrlb  20022  aannenlem3  20114  dvrelog  20395  logcn  20405  logccv  20421  ppiub  20855  lgsquadlem1  21005  lgsquadlem2  21006  dirith2  21089  usgraexmpldifpr  21285  usgraexmpl  21286  konigsberg  21557  nvrel  21929  phrel  22164  bnrel  22217  hlrel  22240  pjnormi  23071  lnopunilem1  23361  lnophmlem1  23367  ssnnssfz  23984  xrge0iifiso  24125  erdszelem4  24659  erdszelem8  24663  supfz  24978  inffz  24979  elrn3  25144  omsinds  25243  naim1i  25850  naim2i  25851  mont  25873  onpsstopbas  25894  wl-bitri  25935  trer  26010  fneer  26059  incsequz2  26144  cncfres  26165  heiborlem3  26213  rencldnfilem  26572  pellexlem4  26586  pellexlem5  26587  jm2.23  26758  ttac  26798  idomsubgmo  27183  lhe4.4ex1a  27215  onfrALTlem5  27971  eel0001  28171  eel0000  28172  eel00001  28174  eel00000  28175  e000  28220  e00  28221  bnj1023  28489  bnj1109  28495  diclspsn  31309  dih1dimatlem  31444
This theorem was proved from axioms:  ax-mp 8
  Copyright terms: Public domain W3C validator