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  197  imbi12i  338  pm3.2i  469  minimp-sylsimp  1551  minimp-ax2c  1553  minimp-ax2  1554  minimp-pm2.43  1555  sbcom2  2337  sstri  3481  0disj  4473  disjx0  4475  relres  5237  cnvdif  5348  difxp  5367  funopab4  5724  fun0  5753  fvsn  6227  omsinds  6850  reltpos  7117  tpostpos  7132  tpos0  7142  oaabs2  7486  swoer  7533  xpider  7579  erinxp  7582  sbthcl  7841  php  7903  elirrv  8261  inf0  8275  unctb  8784  fin1a2lem12  8990  axcc2lem  9015  axcclem  9036  brdom3  9105  brdom5  9106  brdom4  9107  pwcfsdom  9158  smobeth  9161  fpwwe2lem8  9212  fpwwe2lem9  9213  fpwwe2lem12  9216  pwxpndom2  9240  pwcdandom  9242  gchac  9256  wunex3  9316  inar1  9350  gruina  9393  ltsopi  9463  recmulnq  9539  prcdnq  9568  ltrel  9848  lerel  9850  suprfinzcl  11230  cnexALT  11566  dfle2  11721  dflt2  11722  uzrdg0i  12484  ltwefz  12488  fzennn  12493  faclbnd4lem1  12806  hashsslei  12933  0csh0  13244  isercolllem1  14104  zsum  14160  sum0  14163  znnen  14644  qnnen  14645  rpnnen  14659  ruc  14675  nthruc  14683  nthruz  14684  phicl2  15193  pwsle  15863  xpsc0  15939  xpsc1  15940  relfull  16287  relfth  16288  gicer  17437  gicerOLD  17438  oppglsm  17792  efgrelexlemb  17898  isunit  18391  opsrtoslem2  19214  xrsnsgrp  19509  pjpm  19778  1stcfb  20965  2ndc1stc  20971  2ndcctbss  20975  2ndcdisj2  20977  2ndcsep  20979  hmpher  21304  met1stc  22042  re2ndc  22325  iccpnfhmeo  22479  xrhmeo  22480  xrcmp  22482  xrcon  22483  dyadmbl  23060  opnmblALT  23063  vitalilem2  23070  vitalilem3  23071  vitali  23074  mbfimaopnlem  23114  mbfsup  23123  dgrval  23683  dgrcl  23688  dgrub  23689  dgrlb  23691  aannenlem3  23787  dvrelog  24081  logcn  24091  logccv  24107  logblog  24228  ppiub  24629  lgsquadlem1  24805  lgsquadlem2  24806  dirith2  24917  usgraexmpldifpr  25677  usgraexmplef  25678  disjxwwlks  26013  disjxwwlkn  26022  konigsberg  26263  nvrel  26608  phrel  26843  bnrel  26896  hlrel  26929  pjnormi  27763  lnopunilem1  28052  lnophmlem1  28058  xrge0infssd  28718  xrge0infssdOLD  28719  infxrge0lb  28722  infxrge0lbOLD  28723  infxrge0glb  28724  infxrge0glbOLD  28725  infxrge0gelb  28726  infxrge0gelbOLD  28727  ssnnssfz  28743  xrge0iifiso  29116  omsf  29494  omsfOLD  29498  oms0  29499  omssubaddlem  29501  omssubadd  29502  oms0OLD  29503  omssubaddlemOLD  29505  omssubaddOLD  29506  oddpwdc  29561  bnj1023  29961  bnj1109  29967  erdszelem4  30286  erdszelem8  30290  supfz  30720  inffz  30721  elrn3  30759  trer  31326  fneer  31363  naim1i  31401  naim2i  31402  mont  31423  onpsstopbas  31444  bj-mp2c  31546  bj-mp2d  31547  bj-currypeirce  31559  wl-equsal1i  32374  wl-sbcom2d  32389  poimirlem25  32470  poimirlem26  32471  mblfinlem1  32482  incsequz2  32581  cncfres  32600  heiborlem3  32648  diclspsn  35367  dih1dimatlem  35502  rencldnfilem  36268  pellexlem4  36280  pellexlem5  36281  ttac  36491  idomsubgmo  36672  areaquad  36698  frege102  37156  lhe4.4ex1a  37427  eel0001  37843  eel0000  37844  eel00001  37846  eel00000  37847  e000  37892  e00  37893  fzisoeu  38336  resincncf  38646  fmtnoinf  39880  disjxwwlksn  41201  av-disjxwwlkn  41210  ssnn0ssfz  42011  zlmodzxzldeplem  42172
  Copyright terms: Public domain W3C validator