MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mp2 Structured version   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  3349  0disj  4197  disjx0  4199  relres  5166  cnvdif  5270  funopab4  5480  fun0  5500  fvsn  5918  difxp  6372  reltpos  6476  tpostpos  6491  tpos0  6501  oaabs2  6880  swoer  6925  xpider  6967  erinxp  6970  sbthcl  7221  php  7283  inf0  7566  unctb  8075  fin1a2lem12  8281  axcc2lem  8306  axcclem  8327  brdom3  8396  brdom5  8397  brdom4  8398  pwcfsdom  8448  smobeth  8451  fpwwe2lem8  8502  fpwwe2lem9  8503  fpwwe2lem12  8506  pwxpndom2  8530  pwcdandom  8532  gchac  8538  wunex3  8606  inar1  8640  gruina  8683  ltsopi  8755  recmulnq  8831  prcdnq  8860  ltrel  9130  lerel  9132  cnexALT  10598  dfle2  10730  dflt2  10731  uzrdg0i  11289  ltwefz  11293  fzennn  11297  faclbnd4lem1  11574  hashsslei  11675  isercolllem1  12448  zsum  12502  sum0  12505  xpnnenOLD  12799  znnen  12802  qnnen  12803  rpnnen  12816  ruc  12832  nthruc  12840  nthruz  12841  phicl2  13147  pwsle  13704  xpsc0  13775  xpsc1  13776  relfull  14095  relfth  14096  gicer  15053  oppglsm  15266  efgrelexlemb  15372  isunit  15752  opsrtoslem2  16535  pjpm  16925  1stcfb  17498  2ndc1stc  17504  2ndcctbss  17508  2ndcdisj2  17510  2ndcsep  17512  hmpher  17806  met1stc  18541  re2ndc  18822  iccpnfhmeo  18960  xrhmeo  18961  xrcmp  18963  xrcon  18964  dyadmbl  19482  opnmblALT  19485  vitalilem2  19491  vitalilem3  19492  vitali  19495  mbfimaopnlem  19537  mbfsup  19546  dgrval  20137  dgrcl  20142  dgrub  20143  dgrlb  20145  aannenlem3  20237  dvrelog  20518  logcn  20528  logccv  20544  ppiub  20978  lgsquadlem1  21128  lgsquadlem2  21129  dirith2  21212  usgraexmpldifpr  21409  usgraexmpl  21410  konigsberg  21699  nvrel  22071  phrel  22306  bnrel  22359  hlrel  22382  pjnormi  23213  lnopunilem1  23503  lnophmlem1  23509  ssnnssfz  24138  xrge0iifiso  24311  erdszelem4  24870  erdszelem8  24874  supfz  25189  inffz  25190  elrn3  25376  omsinds  25479  naim1i  26101  naim2i  26102  mont  26124  onpsstopbas  26145  wl-bitri  26186  mblfinlem  26207  trer  26273  fneer  26322  incsequz2  26407  cncfres  26428  heiborlem3  26476  rencldnfilem  26835  pellexlem4  26849  pellexlem5  26850  jm2.23  27021  ttac  27061  idomsubgmo  27446  lhe4.4ex1a  27478  onfrALTlem5  28529  eel0001  28731  eel0000  28732  eel00001  28734  eel00000  28735  e000  28780  e00  28781  bnj1023  29052  bnj1109  29058  diclspsn  31893  dih1dimatlem  32028
This theorem was proved from axioms:  ax-mp 8
  Copyright terms: Public domain W3C validator