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  3944  0disj  5092  disjx0  5094  opthhausdorff  5466  relres  5965  cnvdif  6102  difxp  6123  funopab4  6530  fun0  6558  omsinds  7831  frxp3  8095  reltpos  8175  tpos0  8200  oaabs2  8579  swoer  8669  xpider  8729  sbthcl  9031  elirrvOLD  9507  unctb  10118  fin1a2lem12  10325  axcc2lem  10350  axcclem  10371  brdom3  10442  brdom5  10443  brdom4  10444  pwcfsdom  10498  smobeth  10501  pwxpndom2  10580  pwdjundom  10582  gchac  10596  wunex3  10656  inar1  10690  gruina  10733  ltsopi  10803  recmulnq  10879  prcdnq  10908  ltrel  11198  lerel  11200  suprfinzcl  12610  cnexALT  12903  dfle2  13065  dflt2  13066  uzrdg0i  13886  ltwefz  13890  fzennn  13895  faclbnd4lem1  14220  hashsslei  14353  0csh0  14720  isercolllem1  15592  zsum  15645  sum0  15648  znnen  16141  qnnen  16142  rpnnen  16156  ruc  16172  nthruc  16181  nthruz  16182  phicl2  16699  relfull  17838  relfth  17839  gicer  19210  oppglsm  19575  efgrelexlemb  19683  isunit  20313  xrsnsgrp  21366  pjpm  21667  1stcfb  23393  2ndc1stc  23399  2ndcctbss  23403  2ndcdisj2  23405  2ndcsep  23407  hmpher  23732  met1stc  24469  re2ndc  24749  iccpnfhmeo  24903  xrhmeo  24904  xrcmp  24906  xrconn  24907  dyadmbl  25561  opnmblALT  25564  vitalilem2  25570  vitalilem3  25571  vitali  25574  mbfimaopnlem  25616  mbfsup  25625  dgrval  26193  dgrcl  26198  dgrub  26199  dgrlb  26201  aannenlem3  26298  dvrelog  26606  logcn  26616  logccv  26632  ppiub  27175  lgsquadlem1  27351  lgsquadlem2  27352  addsqrexnreu  27413  addsqnreup  27414  2sqreunnlem2  27426  dirith2  27499  madefi  27895  bdayfinbndlem1  28446  usgrexmpldifpr  29314  usgrexmplef  29315  disjxwwlksn  29960  disjxwwlkn  29969  nvrel  30660  phrel  30873  bnrel  30925  hlrel  30948  pjnormi  31779  lnopunilem1  32068  lnophmlem1  32074  xrge0infssd  32822  infxrge0lb  32825  infxrge0glb  32826  infxrge0gelb  32827  ssnnssfz  32848  xrge0iifiso  34073  omsf  34434  oms0  34435  omssubaddlem  34437  omssubadd  34438  oddpwdc  34492  rpsqrtcn  34731  bnj1023  34917  bnj1109  34923  erdszelem4  35369  erdszelem8  35373  gonan0  35567  2thALT  35859  supfz  35904  inffz  35905  trer  36491  fneer  36528  naim1i  36566  naim2i  36567  nmotru  36583  onpsstopbas  36605  bj-mp2c  36715  bj-mp2d  36716  bj-bijust00  36752  bj-cbvalim  36820  bj-cbvexim  36821  bj-cbvalimi  36822  bj-cbveximi  36823  iccioo01  37503  pibt2  37593  wl-equsal1i  37720  wl-sbcom2d  37737  poimirlem25  37817  poimirlem26  37818  mblfinlem1  37829  incsequz2  37921  cncfres  37937  heiborlem3  37985  diclspsn  41491  dih1dimatlem  41626  rencldnfilem  43098  pellexlem4  43110  pellexlem5  43111  ttac  43314  idomsubgmo  43471  areaquad  43494  frege102  44242  lhe4.4ex1a  44606  eel0000  44996  eel00001  44997  eel00000  44998  e000  45043  e00  45044  wffr  45238  modelaxreplem1  45255  nregmodellem  45293  fzisoeu  45584  resincncf  46155  nthrucw  47166  aiota0def  47378  fvmptrabdm  47575  fmtnoinf  47818  gricrel  48201  grlicrel  48288  usgrexmpl1lem  48303  usgrexmpl2lem  48308  usgrexmpl2nb0  48313  usgrexmpl2nb1  48314  usgrexmpl2nb2  48315  usgrexmpl2nb3  48316  usgrexmpl2nb4  48317  usgrexmpl2nb5  48318  gpgprismgr4cycllem2  48378  gpg5ngric  48410  ssnn0ssfz  48631  zlmodzxzldeplem  48780  tposideq  49169