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

Theorem mp2 9
Description: A double modus ponens inference. (Contributed by NM, 5-Apr-1994.)
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 was proved from axioms:  ax-mp 5
This theorem is referenced by:  impbii  199  imbi12i  340  pm3.2i  471  minimp-sylsimp  1558  minimp-ax2c  1560  minimp-ax2  1561  minimp-pm2.43  1562  sbcom2  2444  sstri  3597  0disj  4615  disjx0  4617  relres  5395  cnvdif  5508  difxp  5527  funopab4  5893  fun0  5922  fvsn  6411  omsinds  7046  reltpos  7317  tpostpos  7332  tpos0  7342  oaabs2  7685  swoer  7732  xpider  7778  erinxp  7781  sbthcl  8042  php  8104  elirrv  8464  inf0  8478  unctb  8987  fin1a2lem12  9193  axcc2lem  9218  axcclem  9239  brdom3  9310  brdom5  9311  brdom4  9312  pwcfsdom  9365  smobeth  9368  fpwwe2lem8  9419  fpwwe2lem9  9420  fpwwe2lem12  9423  pwxpndom2  9447  pwcdandom  9449  gchac  9463  wunex3  9523  inar1  9557  gruina  9600  ltsopi  9670  recmulnq  9746  prcdnq  9775  ltrel  10060  lerel  10062  suprfinzcl  11452  cnexALT  11788  dfle2  11940  dflt2  11941  uzrdg0i  12714  ltwefz  12718  fzennn  12723  faclbnd4lem1  13036  hashsslei  13169  0csh0  13492  isercolllem1  14345  zsum  14398  sum0  14401  znnen  14885  qnnen  14886  rpnnen  14900  ruc  14916  nthruc  14924  nthruz  14925  phicl2  15416  pwsle  16092  xpsc0  16160  xpsc1  16161  relfull  16508  relfth  16509  gicer  17658  gicerOLD  17659  oppglsm  17997  efgrelexlemb  18103  isunit  18597  opsrtoslem2  19425  xrsnsgrp  19722  pjpm  19992  1stcfb  21188  2ndc1stc  21194  2ndcctbss  21198  2ndcdisj2  21200  2ndcsep  21202  hmpher  21527  met1stc  22266  re2ndc  22544  iccpnfhmeo  22684  xrhmeo  22685  xrcmp  22687  xrconn  22688  dyadmbl  23308  opnmblALT  23311  vitalilem2  23318  vitalilem3  23319  vitali  23322  mbfimaopnlem  23362  mbfsup  23371  dgrval  23922  dgrcl  23927  dgrub  23928  dgrlb  23930  aannenlem3  24023  dvrelog  24317  logcn  24327  logccv  24343  logblog  24464  ppiub  24863  lgsquadlem1  25039  lgsquadlem2  25040  dirith2  25151  usgrexmpldifpr  26077  usgrexmplef  26078  disjxwwlksn  26702  disjxwwlkn  26711  nvrel  27345  phrel  27558  bnrel  27611  hlrel  27634  pjnormi  28468  lnopunilem1  28757  lnophmlem1  28763  xrge0infssd  29411  infxrge0lb  29414  infxrge0glb  29415  infxrge0gelb  29416  ssnnssfz  29432  xrge0iifiso  29805  omsf  30181  oms0  30182  omssubaddlem  30184  omssubadd  30185  oddpwdc  30239  bnj1023  30612  bnj1109  30618  erdszelem4  30937  erdszelem8  30941  supfz  31374  inffz  31375  inffzOLD  31376  elrn3  31414  trer  32005  fneer  32043  naim1i  32081  naim2i  32082  mont  32103  onpsstopbas  32124  bj-mp2c  32226  bj-mp2d  32227  bj-currypeirce  32239  wl-equsal1i  33000  wl-sbcom2d  33015  poimirlem25  33105  poimirlem26  33106  mblfinlem1  33117  incsequz2  33216  cncfres  33235  heiborlem3  33283  diclspsn  36002  dih1dimatlem  36137  rencldnfilem  36903  pellexlem4  36915  pellexlem5  36916  ttac  37122  idomsubgmo  37296  areaquad  37322  frege102  37780  lhe4.4ex1a  38049  eel0001  38466  eel0000  38467  eel00001  38469  eel00000  38470  e000  38515  e00  38516  fzisoeu  39013  resincncf  39423  fmtnoinf  40777  ssnn0ssfz  41445  zlmodzxzldeplem  41605
  Copyright terms: Public domain W3C validator