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 ⊢ 𝜒

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5

This theorem is used by:  impbii  212  imbi12i  353  pm3.2i  476  minimp-syllsimp  1654  minimp-ax2c  1656  minimp-ax2  1657  minimp-pm2.43  1658  darii  2689  barbarilem  2692  festino  2698  baroco  2700  darapti  2708  sstri  3917  0disj  5095  disjx0  5097  opthhausdorff  5489  relres  5995  cnvdif  6133  difxp  6154  funopab4  6577  fun0  6605  omsinds  7898  frxp3  8168  reltpos  8249  tpos0  8274  oaabs2  8659  swoer  8750  xpider  8810  sbthcl  9119  elirrvOLDOLD  9594  unctb  10283  fin1a2lem12  10490  axcc2lem  10515  axcclem  10536  brdom3  10608  brdom5  10609  brdom4  10610  pwcfsdom  10669  smobeth  10672  pwxpndom2  10751  pwdjundom  10753  gchac  10767  wunex3  10827  inar1  10861  gruina  10904  ltsopi  10974  recmulnq  11050  prcdnq  11079  ltrel  11372  lerel  11374  suprfinzcl  12814  cnexALT  13115  dfle2  13277  dflt2  13278  uzrdg0i  14103  ltwefz  14107  fzennn  14112  faclbnd4lem1  14438  hashsslei  14572  0csh0  14945  isercolllem1  15833  zsum  15885  sum0  15888  znnen  16381  qnnen  16382  rpnnen  16396  ruc  16412  nthruc  16421  nthruz  16422  phicl2  16946  relfull  18086  relfth  18087  gicer  19492  oppglsm  19857  efgrelexlemb  19965  isunit  20604  ricrel  20745  xrsnsgrp  21715  pjpm  22015  1stcfb  23764  2ndc1stc  23770  2ndcctbss  23775  2ndcdisj2  23777  2ndcsep  23779  hmpher  24104  met1stc  24841  re2ndc  25121  iccpnfhmeo  25267  xrhmeo  25268  xrcmp  25270  xrconn  25271  dyadmbl  25922  opnmblALT  25925  vitalilem2  25931  vitalilem3  25932  vitali  25935  mbfimaopnlem  25977  mbfsup  25986  dgrval  26548  dgrcl  26553  dgrub  26554  dgrlb  26556  aannenlem3  26658  dvrelog  26966  logcn  26976  logccv  26992  ppiub  27532  lgsquadlem1  27708  lgsquadlem2  27709  addsqrexnreu  27770  addsqnreup  27771  2sqreunnlem2  27783  dirith2  27856  bdayfinbndlem1  28854  usgrexmpldifpr  29840  usgrexmplef  29841  disjxwwlksn  30494  disjxwwlkn  30503  nvrel  31205  phrel  31418  bnrel  31470  hlrel  31493  pjnormi  32324  lnopunilem1  32613  lnophmlem1  32619  xrge0infssd  33396  infxrge0lb  33399  infxrge0glb  33400  infxrge0gelb  33401  ssnnssfz  33422  xrge0iifiso  34610  omsf  34971  oms0  34972  omssubaddlem  34974  omssubadd  34975  oddpwdc  35029  rpsqrtcn  35265  bnj1023  35454  bnj1109  35460  erdszelem4  36028  erdszelem8  36032  gonan0  36226  2thALT  36518  onprcr  36531  supfz  36569  inffz  36570  trer  37179  fneer  37216  naim1i  37254  naim2i  37255  nmotru  37271  onpsstopbas  37293  bj-mp2c  37481  bj-mp2d  37482  bj-bijust00  37522  bj-almp  37556  bj-axseprep  38065  iccioo01  38326  pibt2  38416  wl-equsal1i  38552  wl-sbcom2d  38569  poimirlem25  38639  poimirlem26  38640  mblfinlem1  38651  incsequz2  38759  cncfres  38775  heiborlem3  38823  diclspsn  42327  dih1dimatlem  42462  rencldnfilem  43903  pellexlem4  43915  pellexlem5  43916  ttac  44119  idomsubgmo  44271  areaquad  44294  frege102  45041  lhe4.4ex1a  45389  eel0000  45778  eel00001  45779  eel00000  45780  e000  45825  e00  45826  wffr  46027  modelaxreplem1  46044  nregmodellem  46082  fzisoeu  46392  resincncf  46961  numtowerdt  47992  aiota0def  48242  fvmptrabdm  48439  fmtnoinf  48697  gricrel  49093  grlicrel  49180  usgrexmpl1lem  49195  usgrexmpl2lem  49200  usgrexmpl2nb0  49205  usgrexmpl2nb1  49206  usgrexmpl2nb2  49207  usgrexmpl2nb3  49208  usgrexmpl2nb4  49209  usgrexmpl2nb5  49210  gpgprismgr4cycllem2  49270  gpg5ngric  49302  ssnn0ssfz  49537  zlmodzxzldeplem  49686  tposideq  50072