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

Step	Hyp	Ref	Expression
1		mp2.2	. 2 ⊢ 𝜓
2		mp2.1	. . 3 ⊢ 𝜑
3		mp2.3	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
4	2, 3	ax-mp 5	. 2 ⊢ (𝜓 → 𝜒)
5	1, 4	ax-mp 5	1 ⊢ 𝜒

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5

This theorem is referenced by:  impbii  209  imbi12i  350  pm3.2i  470  minimp-syllsimp  1622  minimp-ax2c  1624  minimp-ax2  1625  minimp-pm2.43  1626  darii  2658  barbarilem  2661  festino  2667  baroco  2669  darapti  2677  sstri  3956  0disj  5100  disjx0  5102  opthhausdorff  5477  relres  5976  cnvdif  6116  difxp  6137  funopab4  6553  fun0  6581  omsinds  7863  frxp3  8130  reltpos  8210  tpos0  8235  oaabs2  8613  swoer  8702  xpider  8761  sbthcl  9063  elirrv  9549  unctb  10157  fin1a2lem12  10364  axcc2lem  10389  axcclem  10410  brdom3  10481  brdom5  10482  brdom4  10483  pwcfsdom  10536  smobeth  10539  pwxpndom2  10618  pwdjundom  10620  gchac  10634  wunex3  10694  inar1  10728  gruina  10771  ltsopi  10841  recmulnq  10917  prcdnq  10946  ltrel  11236  lerel  11238  suprfinzcl  12648  cnexALT  12945  dfle2  13107  dflt2  13108  uzrdg0i  13924  ltwefz  13928  fzennn  13933  faclbnd4lem1  14258  hashsslei  14391  0csh0  14758  isercolllem1  15631  zsum  15684  sum0  15687  znnen  16180  qnnen  16181  rpnnen  16195  ruc  16211  nthruc  16220  nthruz  16221  phicl2  16738  relfull  17872  relfth  17873  gicer  19209  oppglsm  19572  efgrelexlemb  19680  isunit  20282  xrsnsgrp  21319  pjpm  21617  1stcfb  23332  2ndc1stc  23338  2ndcctbss  23342  2ndcdisj2  23344  2ndcsep  23346  hmpher  23671  met1stc  24409  re2ndc  24689  iccpnfhmeo  24843  xrhmeo  24844  xrcmp  24846  xrconn  24847  dyadmbl  25501  opnmblALT  25504  vitalilem2  25510  vitalilem3  25511  vitali  25514  mbfimaopnlem  25556  mbfsup  25565  dgrval  26133  dgrcl  26138  dgrub  26139  dgrlb  26141  aannenlem3  26238  dvrelog  26546  logcn  26556  logccv  26572  ppiub  27115  lgsquadlem1  27291  lgsquadlem2  27292  addsqrexnreu  27353  addsqnreup  27354  2sqreunnlem2  27366  dirith2  27439  madefi  27824  usgrexmpldifpr  29185  usgrexmplef  29186  disjxwwlksn  29834  disjxwwlkn  29843  nvrel  30531  phrel  30744  bnrel  30796  hlrel  30819  pjnormi  31650  lnopunilem1  31939  lnophmlem1  31945  xrge0infssd  32684  infxrge0lb  32687  infxrge0glb  32688  infxrge0gelb  32689  ssnnssfz  32710  xrge0iifiso  33925  omsf  34287  oms0  34288  omssubaddlem  34290  omssubadd  34291  oddpwdc  34345  rpsqrtcn  34584  bnj1023  34770  bnj1109  34776  erdszelem4  35181  erdszelem8  35185  gonan0  35379  2thALT  35671  supfz  35716  inffz  35717  trer  36304  fneer  36341  naim1i  36379  naim2i  36380  nmotru  36396  onpsstopbas  36418  bj-mp2c  36528  bj-mp2d  36529  bj-bijust00  36565  bj-cbvalim  36633  bj-cbvexim  36634  bj-cbvalimi  36635  bj-cbveximi  36636  iccioo01  37315  pibt2  37405  wl-equsal1i  37532  wl-sbcom2d  37549  poimirlem25  37639  poimirlem26  37640  mblfinlem1  37651  incsequz2  37743  cncfres  37759  heiborlem3  37807  diclspsn  41188  dih1dimatlem  41323  rencldnfilem  42808  pellexlem4  42820  pellexlem5  42821  ttac  43025  idomsubgmo  43182  areaquad  43205  frege102  43954  lhe4.4ex1a  44318  eel0000  44709  eel00001  44710  eel00000  44711  e000  44756  e00  44757  wffr  44951  modelaxreplem1  44968  nregmodellem  45006  fzisoeu  45298  resincncf  45873  aiota0def  47097  fvmptrabdm  47294  fmtnoinf  47537  gricrel  47919  grlicrel  47998  usgrexmpl1lem  48012  usgrexmpl2lem  48017  usgrexmpl2nb0  48022  usgrexmpl2nb1  48023  usgrexmpl2nb2  48024  usgrexmpl2nb3  48025  usgrexmpl2nb4  48026  usgrexmpl2nb5  48027  gpgprismgr4cycllem2  48086  gpg5ngric  48118  ssnn0ssfz  48337  zlmodzxzldeplem  48487  tposideq  48876