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  1624  minimp-ax2c  1626  minimp-ax2  1627  minimp-pm2.43  1628  darii  2666  barbarilem  2669  festino  2675  baroco  2677  darapti  2685  sstri  3945  0disj  5093  disjx0  5095  opthhausdorff  5473  relres  5972  cnvdif  6109  difxp  6130  funopab4  6537  fun0  6565  omsinds  7839  frxp3  8103  reltpos  8183  tpos0  8208  oaabs2  8587  swoer  8677  xpider  8737  sbthcl  9039  elirrvOLD  9515  unctb  10126  fin1a2lem12  10333  axcc2lem  10358  axcclem  10379  brdom3  10450  brdom5  10451  brdom4  10452  pwcfsdom  10506  smobeth  10509  pwxpndom2  10588  pwdjundom  10590  gchac  10604  wunex3  10664  inar1  10698  gruina  10741  ltsopi  10811  recmulnq  10887  prcdnq  10916  ltrel  11206  lerel  11208  suprfinzcl  12618  cnexALT  12911  dfle2  13073  dflt2  13074  uzrdg0i  13894  ltwefz  13898  fzennn  13903  faclbnd4lem1  14228  hashsslei  14361  0csh0  14728  isercolllem1  15600  zsum  15653  sum0  15656  znnen  16149  qnnen  16150  rpnnen  16164  ruc  16180  nthruc  16189  nthruz  16190  phicl2  16707  relfull  17846  relfth  17847  gicer  19218  oppglsm  19583  efgrelexlemb  19691  isunit  20321  xrsnsgrp  21374  pjpm  21675  1stcfb  23401  2ndc1stc  23407  2ndcctbss  23411  2ndcdisj2  23413  2ndcsep  23415  hmpher  23740  met1stc  24477  re2ndc  24757  iccpnfhmeo  24911  xrhmeo  24912  xrcmp  24914  xrconn  24915  dyadmbl  25569  opnmblALT  25572  vitalilem2  25578  vitalilem3  25579  vitali  25582  mbfimaopnlem  25624  mbfsup  25633  dgrval  26201  dgrcl  26206  dgrub  26207  dgrlb  26209  aannenlem3  26306  dvrelog  26614  logcn  26624  logccv  26640  ppiub  27183  lgsquadlem1  27359  lgsquadlem2  27360  addsqrexnreu  27421  addsqnreup  27422  2sqreunnlem2  27434  dirith2  27507  madefi  27921  bdayfinbndlem1  28475  usgrexmpldifpr  29343  usgrexmplef  29344  disjxwwlksn  29989  disjxwwlkn  29998  nvrel  30689  phrel  30902  bnrel  30954  hlrel  30977  pjnormi  31808  lnopunilem1  32097  lnophmlem1  32103  xrge0infssd  32851  infxrge0lb  32854  infxrge0glb  32855  infxrge0gelb  32856  ssnnssfz  32877  xrge0iifiso  34112  omsf  34473  oms0  34474  omssubaddlem  34476  omssubadd  34477  oddpwdc  34531  rpsqrtcn  34770  bnj1023  34956  bnj1109  34962  erdszelem4  35407  erdszelem8  35411  gonan0  35605  2thALT  35897  supfz  35942  inffz  35943  trer  36529  fneer  36566  naim1i  36604  naim2i  36605  nmotru  36621  onpsstopbas  36643  bj-mp2c  36759  bj-mp2d  36760  bj-bijust00  36798  bj-almp  36832  bj-cbvalim  36882  bj-cbvexim  36883  bj-cbvalimi  36884  bj-cbveximi  36885  bj-axseprep  37313  iccioo01  37571  pibt2  37661  wl-equsal1i  37788  wl-sbcom2d  37805  poimirlem25  37885  poimirlem26  37886  mblfinlem1  37897  incsequz2  37989  cncfres  38005  heiborlem3  38053  diclspsn  41559  dih1dimatlem  41694  rencldnfilem  43166  pellexlem4  43178  pellexlem5  43179  ttac  43382  idomsubgmo  43539  areaquad  43562  frege102  44310  lhe4.4ex1a  44674  eel0000  45064  eel00001  45065  eel00000  45066  e000  45111  e00  45112  wffr  45306  modelaxreplem1  45323  nregmodellem  45361  fzisoeu  45651  resincncf  46222  nthrucw  47233  aiota0def  47445  fvmptrabdm  47642  fmtnoinf  47885  gricrel  48268  grlicrel  48355  usgrexmpl1lem  48370  usgrexmpl2lem  48375  usgrexmpl2nb0  48380  usgrexmpl2nb1  48381  usgrexmpl2nb2  48382  usgrexmpl2nb3  48383  usgrexmpl2nb4  48384  usgrexmpl2nb5  48385  gpgprismgr4cycllem2  48445  gpg5ngric  48477  ssnn0ssfz  48698  zlmodzxzldeplem  48847  tposideq  49236