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  1618  minimp-ax2c  1620  minimp-ax2  1621  minimp-pm2.43  1622  darii  2662  barbarilem  2665  festino  2671  baroco  2673  darapti  2681  sstri  4004  0disj  5140  disjx0  5142  opthhausdorff  5526  relres  6025  cnvdif  6165  difxp  6185  funopab4  6604  fun0  6632  omsinds  7907  omsindsOLD  7908  frxp3  8174  reltpos  8254  tpos0  8279  oaabs2  8685  swoer  8774  xpider  8826  sbthcl  9133  phpOLD  9256  elirrv  9633  unctb  10241  fin1a2lem12  10448  axcc2lem  10473  axcclem  10494  brdom3  10565  brdom5  10566  brdom4  10567  pwcfsdom  10620  smobeth  10623  pwxpndom2  10702  pwdjundom  10704  gchac  10718  wunex3  10778  inar1  10812  gruina  10855  ltsopi  10925  recmulnq  11001  prcdnq  11030  ltrel  11320  lerel  11322  suprfinzcl  12729  cnexALT  13025  dfle2  13185  dflt2  13186  uzrdg0i  13996  ltwefz  14000  fzennn  14005  faclbnd4lem1  14328  hashsslei  14461  0csh0  14827  isercolllem1  15697  zsum  15750  sum0  15753  znnen  16244  qnnen  16245  rpnnen  16259  ruc  16275  nthruc  16284  nthruz  16285  phicl2  16801  relfull  17961  relfth  17962  gicer  19307  oppglsm  19674  efgrelexlemb  19782  isunit  20389  xrsnsgrp  21437  pjpm  21745  1stcfb  23468  2ndc1stc  23474  2ndcctbss  23478  2ndcdisj2  23480  2ndcsep  23482  hmpher  23807  met1stc  24549  re2ndc  24836  iccpnfhmeo  24989  xrhmeo  24990  xrcmp  24992  xrconn  24993  dyadmbl  25648  opnmblALT  25651  vitalilem2  25657  vitalilem3  25658  vitali  25661  mbfimaopnlem  25703  mbfsup  25712  dgrval  26281  dgrcl  26286  dgrub  26287  dgrlb  26289  aannenlem3  26386  dvrelog  26693  logcn  26703  logccv  26719  ppiub  27262  lgsquadlem1  27438  lgsquadlem2  27439  addsqrexnreu  27500  addsqnreup  27501  2sqreunnlem2  27513  dirith2  27586  madefi  27964  usgrexmpldifpr  29289  usgrexmplef  29290  disjxwwlksn  29933  disjxwwlkn  29942  nvrel  30630  phrel  30843  bnrel  30895  hlrel  30918  pjnormi  31749  lnopunilem1  32038  lnophmlem1  32044  xrge0infssd  32771  infxrge0lb  32774  infxrge0glb  32775  infxrge0gelb  32776  ssnnssfz  32795  xrge0iifiso  33895  omsf  34277  oms0  34278  omssubaddlem  34280  omssubadd  34281  oddpwdc  34335  rpsqrtcn  34586  bnj1023  34772  bnj1109  34778  erdszelem4  35178  erdszelem8  35182  gonan0  35376  2thALT  35668  supfz  35708  inffz  35709  trer  36298  fneer  36335  naim1i  36373  naim2i  36374  nmotru  36390  onpsstopbas  36412  bj-mp2c  36522  bj-mp2d  36523  bj-bijust00  36559  bj-cbvalim  36627  bj-cbvexim  36628  bj-cbvalimi  36629  bj-cbveximi  36630  iccioo01  37309  pibt2  37399  wl-equsal1i  37524  wl-sbcom2d  37541  poimirlem25  37631  poimirlem26  37632  mblfinlem1  37643  incsequz2  37735  cncfres  37751  heiborlem3  37799  diclspsn  41176  dih1dimatlem  41311  rencldnfilem  42807  pellexlem4  42819  pellexlem5  42820  ttac  43024  idomsubgmo  43181  areaquad  43204  frege102  43954  lhe4.4ex1a  44324  eel0000  44717  eel00001  44718  eel00000  44719  e000  44764  e00  44765  modelaxreplem1  44942  fzisoeu  45250  resincncf  45830  aiota0def  47045  fvmptrabdm  47242  fmtnoinf  47460  gricrel  47825  grlicrel  47901  usgrexmpl1lem  47915  usgrexmpl2lem  47920  usgrexmpl2nb0  47925  usgrexmpl2nb1  47926  usgrexmpl2nb2  47927  usgrexmpl2nb3  47928  usgrexmpl2nb4  47929  usgrexmpl2nb5  47930  ssnn0ssfz  48193  zlmodzxzldeplem  48343