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  3932  0disj  5079  disjx0  5081  opthhausdorff  5465  relres  5964  cnvdif  6101  difxp  6122  funopab4  6529  fun0  6557  omsinds  7831  frxp3  8094  reltpos  8174  tpos0  8199  oaabs2  8578  swoer  8668  xpider  8728  sbthcl  9030  elirrvOLD  9506  unctb  10117  fin1a2lem12  10324  axcc2lem  10349  axcclem  10370  brdom3  10441  brdom5  10442  brdom4  10443  pwcfsdom  10497  smobeth  10500  pwxpndom2  10579  pwdjundom  10581  gchac  10595  wunex3  10655  inar1  10689  gruina  10732  ltsopi  10802  recmulnq  10878  prcdnq  10907  ltrel  11198  lerel  11200  suprfinzcl  12634  cnexALT  12927  dfle2  13089  dflt2  13090  uzrdg0i  13912  ltwefz  13916  fzennn  13921  faclbnd4lem1  14246  hashsslei  14379  0csh0  14746  isercolllem1  15618  zsum  15671  sum0  15674  znnen  16170  qnnen  16171  rpnnen  16185  ruc  16201  nthruc  16210  nthruz  16211  phicl2  16729  relfull  17868  relfth  17869  gicer  19243  oppglsm  19608  efgrelexlemb  19716  isunit  20344  xrsnsgrp  21397  pjpm  21698  1stcfb  23420  2ndc1stc  23426  2ndcctbss  23430  2ndcdisj2  23432  2ndcsep  23434  hmpher  23759  met1stc  24496  re2ndc  24776  iccpnfhmeo  24922  xrhmeo  24923  xrcmp  24925  xrconn  24926  dyadmbl  25577  opnmblALT  25580  vitalilem2  25586  vitalilem3  25587  vitali  25590  mbfimaopnlem  25632  mbfsup  25641  dgrval  26203  dgrcl  26208  dgrub  26209  dgrlb  26211  aannenlem3  26307  dvrelog  26614  logcn  26624  logccv  26640  ppiub  27181  lgsquadlem1  27357  lgsquadlem2  27358  addsqrexnreu  27419  addsqnreup  27420  2sqreunnlem2  27432  dirith2  27505  madefi  27919  bdayfinbndlem1  28473  usgrexmpldifpr  29341  usgrexmplef  29342  disjxwwlksn  29987  disjxwwlkn  29996  nvrel  30688  phrel  30901  bnrel  30953  hlrel  30976  pjnormi  31807  lnopunilem1  32096  lnophmlem1  32102  xrge0infssd  32849  infxrge0lb  32852  infxrge0glb  32853  infxrge0gelb  32854  ssnnssfz  32875  xrge0iifiso  34095  omsf  34456  oms0  34457  omssubaddlem  34459  omssubadd  34460  oddpwdc  34514  rpsqrtcn  34753  bnj1023  34939  bnj1109  34945  erdszelem4  35392  erdszelem8  35396  gonan0  35590  2thALT  35882  supfz  35927  inffz  35928  trer  36514  fneer  36551  naim1i  36589  naim2i  36590  nmotru  36606  onpsstopbas  36628  bj-mp2c  36816  bj-mp2d  36817  bj-bijust00  36858  bj-almp  36892  bj-axseprep  37397  iccioo01  37657  pibt2  37747  wl-equsal1i  37883  wl-sbcom2d  37900  poimirlem25  37980  poimirlem26  37981  mblfinlem1  37992  incsequz2  38084  cncfres  38100  heiborlem3  38148  diclspsn  41654  dih1dimatlem  41789  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  45751  resincncf  46321  nthrucw  47332  aiota0def  47556  fvmptrabdm  47753  fmtnoinf  48011  gricrel  48407  grlicrel  48494  usgrexmpl1lem  48509  usgrexmpl2lem  48514  usgrexmpl2nb0  48519  usgrexmpl2nb1  48520  usgrexmpl2nb2  48521  usgrexmpl2nb3  48522  usgrexmpl2nb4  48523  usgrexmpl2nb5  48524  gpgprismgr4cycllem2  48584  gpg5ngric  48616  ssnn0ssfz  48837  zlmodzxzldeplem  48986  tposideq  49375