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. (Contributed by NM, 5-Apr-1994.) (Proof modification is discouraged.)
Hypotheses
Ref Expression
mp2.1
mp2.2
mp2.3
Assertion
Ref Expression
mp2

Proof of Theorem mp2
StepHypRef Expression
1 mp2.2 . 2
2 mp2.1 . . 3
3 mp2.3 . . 3
42, 3ax-mp 5 . 2
51, 4ax-mp 5 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4
This theorem is referenced by:  impbii  188  imbi12i  326  pm3.2i  455  sbcom2  2189  sstri  3512  0disj  4445  disjx0  4447  relres  5306  cnvdif  5417  difxp  5436  funopab4  5628  fun0  5650  fvsn  6104  reltpos  6979  tpostpos  6994  tpos0  7004  oaabs2  7313  swoer  7358  xpider  7401  erinxp  7404  sbthcl  7659  php  7721  inf0  8059  unctb  8606  fin1a2lem12  8812  axcc2lem  8837  axcclem  8858  brdom3  8927  brdom5  8928  brdom4  8929  pwcfsdom  8979  smobeth  8982  fpwwe2lem8  9036  fpwwe2lem9  9037  fpwwe2lem12  9040  pwxpndom2  9064  pwcdandom  9066  gchac  9080  wunex3  9140  inar1  9174  gruina  9217  ltsopi  9287  recmulnq  9363  prcdnq  9392  ltrel  9670  lerel  9672  suprfinzcl  11003  cnexALT  11245  dfle2  11382  dflt2  11383  uzrdg0i  12070  ltwefz  12074  fzennn  12078  faclbnd4lem1  12371  hashsslei  12484  0csh0  12764  isercolllem1  13487  zsum  13540  sum0  13543  xpnnenOLD  13943  znnen  13946  qnnen  13947  rpnnen  13960  ruc  13976  nthruc  13984  nthruz  13985  phicl2  14298  pwsle  14889  xpsc0  14957  xpsc1  14958  relfull  15277  relfth  15278  gicer  16324  oppglsm  16662  efgrelexlemb  16768  isunit  17306  opsrtoslem2  18149  xrsnsgrp  18454  pjpm  18739  1stcfb  19946  2ndc1stc  19952  2ndcctbss  19956  2ndcdisj2  19958  2ndcsep  19960  hmpher  20285  met1stc  21024  re2ndc  21306  iccpnfhmeo  21445  xrhmeo  21446  xrcmp  21448  xrcon  21449  dyadmbl  22009  opnmblALT  22012  vitalilem2  22018  vitalilem3  22019  vitali  22022  mbfimaopnlem  22062  mbfsup  22071  dgrval  22625  dgrcl  22630  dgrub  22631  dgrlb  22633  aannenlem3  22726  dvrelog  23018  logcn  23028  logccv  23044  ppiub  23479  lgsquadlem1  23629  lgsquadlem2  23630  dirith2  23713  usgraexmpldifpr  24400  usgraexmpl  24401  disjxwwlks  24736  disjxwwlkn  24745  konigsberg  24987  nvrel  25495  phrel  25730  bnrel  25783  hlrel  25806  pjnormi  26639  lnopunilem1  26929  lnophmlem1  26935  xrge0infssd  27581  ssnnssfz  27597  xrge0iifiso  27917  oms0  28266  oddpwdc  28293  erdszelem4  28638  erdszelem8  28642  supfz  29107  inffz  29108  elrn3  29192  omsinds  29299  naim1i  29852  naim2i  29853  mont  29874  onpsstopbas  29895  wl-equsal1i  29996  wl-sbcom2d  30011  mblfinlem1  30051  trer  30134  fneer  30171  incsequz2  30242  cncfres  30261  heiborlem3  30309  rencldnfilem  30754  pellexlem4  30768  pellexlem5  30769  ttac  30978  idomsubgmo  31155  areaquad  31184  lhe4.4ex1a  31234  fzisoeu  31500  resincncf  31677  ssnn0ssfz  32938  zlmodzxzldeplem  33099  eel0001  33515  eel0000  33516  eel00001  33518  eel00000  33519  e000  33564  e00  33565  bnj1023  33839  bnj1109  33845  bj-mp2c  34129  bj-mp2d  34130  bj-alrimih  34209  diclspsn  36921  dih1dimatlem  37056
This theorem was proved from axioms:  ax-mp 5
  Copyright terms: Public domain W3C validator