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  210  imbi12i  351  pm3.2i  471  minimp-syllsimp  1629  minimp-ax2c  1631  minimp-ax2  1632  minimp-pm2.43  1633  darii  2669  barbarilem  2672  festino  2678  baroco  2680  darapti  2688  sstri  3931  0disj  5072  disjx0  5074  opthhausdorff  5465  relres  5964  cnvdif  6101  difxp  6122  funopab4  6529  fun0  6557  omsinds  7834  frxp3  8098  reltpos  8178  tpos0  8203  oaabs2  8582  swoer  8672  xpider  8732  sbthcl  9034  elirrvOLDOLD  9511  unctb  10124  fin1a2lem12  10331  axcc2lem  10356  axcclem  10377  brdom3  10448  brdom5  10449  brdom4  10450  pwcfsdom  10504  smobeth  10507  pwxpndom2  10586  pwdjundom  10588  gchac  10602  wunex3  10662  inar1  10696  gruina  10739  ltsopi  10809  recmulnq  10885  prcdnq  10914  ltrel  11205  lerel  11207  suprfinzcl  12641  cnexALT  12934  dfle2  13096  dflt2  13097  uzrdg0i  13919  ltwefz  13923  fzennn  13928  faclbnd4lem1  14253  hashsslei  14386  0csh0  14753  isercolllem1  15625  zsum  15678  sum0  15681  znnen  16177  qnnen  16178  rpnnen  16192  ruc  16208  nthruc  16217  nthruz  16218  phicl2  16736  relfull  17875  relfth  17876  gicer  19250  oppglsm  19615  efgrelexlemb  19723  isunit  20351  xrsnsgrp  21390  pjpm  21690  1stcfb  23435  2ndc1stc  23441  2ndcctbss  23445  2ndcdisj2  23447  2ndcsep  23449  hmpher  23774  met1stc  24511  re2ndc  24791  iccpnfhmeo  24937  xrhmeo  24938  xrcmp  24940  xrconn  24941  dyadmbl  25592  opnmblALT  25595  vitalilem2  25601  vitalilem3  25602  vitali  25605  mbfimaopnlem  25647  mbfsup  25656  dgrval  26218  dgrcl  26223  dgrub  26224  dgrlb  26226  aannenlem3  26321  dvrelog  26626  logcn  26636  logccv  26652  ppiub  27192  lgsquadlem1  27368  lgsquadlem2  27369  addsqrexnreu  27430  addsqnreup  27431  2sqreunnlem2  27443  dirith2  27516  madefi  27930  bdayfinbndlem1  28484  usgrexmpldifpr  29352  usgrexmplef  29353  disjxwwlksn  29997  disjxwwlkn  30006  nvrel  30698  phrel  30911  bnrel  30963  hlrel  30986  pjnormi  31817  lnopunilem1  32106  lnophmlem1  32112  xrge0infssd  32860  infxrge0lb  32863  infxrge0glb  32864  infxrge0gelb  32865  ssnnssfz  32886  xrge0iifiso  34126  omsf  34487  oms0  34488  omssubaddlem  34490  omssubadd  34491  oddpwdc  34545  rpsqrtcn  34784  bnj1023  34970  bnj1109  34976  erdszelem4  35423  erdszelem8  35427  gonan0  35621  2thALT  35913  supfz  35958  inffz  35959  trer  36545  fneer  36582  naim1i  36620  naim2i  36621  nmotru  36637  onpsstopbas  36659  bj-mp2c  36847  bj-mp2d  36848  bj-bijust00  36889  bj-almp  36923  bj-axseprep  37428  iccioo01  37690  pibt2  37780  wl-equsal1i  37916  wl-sbcom2d  37933  poimirlem25  38013  poimirlem26  38014  mblfinlem1  38025  incsequz2  38117  cncfres  38133  heiborlem3  38181  diclspsn  41687  dih1dimatlem  41822  rencldnfilem  43266  pellexlem4  43278  pellexlem5  43279  ttac  43482  idomsubgmo  43639  areaquad  43662  frege102  44410  lhe4.4ex1a  44774  eel0000  45164  eel00001  45165  eel00000  45166  e000  45211  e00  45212  wffr  45406  modelaxreplem1  45423  nregmodellem  45461  fzisoeu  45749  resincncf  46319  nthrucw  47332  aiota0def  47560  fvmptrabdm  47757  fmtnoinf  48015  gricrel  48411  grlicrel  48498  usgrexmpl1lem  48513  usgrexmpl2lem  48518  usgrexmpl2nb0  48523  usgrexmpl2nb1  48524  usgrexmpl2nb2  48525  usgrexmpl2nb3  48526  usgrexmpl2nb4  48527  usgrexmpl2nb5  48528  gpgprismgr4cycllem2  48588  gpg5ngric  48620  ssnn0ssfz  48841  zlmodzxzldeplem  48990  tposideq  49379