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  211  imbi12i  352  pm3.2i  474  minimp-syllsimp  1641  minimp-ax2c  1643  minimp-ax2  1644  minimp-pm2.43  1645  darii  2690  barbarilem  2693  festino  2699  baroco  2701  darapti  2709  sstri  3945  0disj  5092  disjx0  5094  opthhausdorff  5485  relres  5989  cnvdif  6122  difxp  6144  funopab4  6552  fun0  6580  omsinds  7861  frxp3  8124  reltpos  8204  tpos0  8229  oaabs2  8612  swoer  8703  xpider  8763  sbthcl  9065  elirrvOLDOLD  9542  unctb  10155  fin1a2lem12  10363  axcc2lem  10388  axcclem  10409  brdom3  10480  brdom5  10481  brdom4  10482  pwcfsdom  10536  smobeth  10539  pwxpndom2  10618  pwdjundom  10620  gchac  10634  wunex3  10694  inar1  10728  gruina  10771  ltsopi  10841  recmulnq  10917  prcdnq  10946  ltrel  11239  lerel  11241  suprfinzcl  12682  cnexALT  12982  dfle2  13144  dflt2  13145  uzrdg0i  13967  ltwefz  13971  fzennn  13976  faclbnd4lem1  14301  hashsslei  14434  0csh0  14801  isercolllem1  15673  zsum  15726  sum0  15729  znnen  16225  qnnen  16226  rpnnen  16240  ruc  16256  nthruc  16265  nthruz  16266  phicl2  16784  relfull  17924  relfth  17925  gicer  19298  oppglsm  19663  efgrelexlemb  19771  isunit  20399  xrsnsgrp  21438  pjpm  21738  1stcfb  23483  2ndc1stc  23489  2ndcctbss  23493  2ndcdisj2  23495  2ndcsep  23497  hmpher  23822  met1stc  24559  re2ndc  24839  iccpnfhmeo  24985  xrhmeo  24986  xrcmp  24988  xrconn  24989  dyadmbl  25640  opnmblALT  25643  vitalilem2  25649  vitalilem3  25650  vitali  25653  mbfimaopnlem  25695  mbfsup  25704  dgrval  26266  dgrcl  26271  dgrub  26272  dgrlb  26274  aannenlem3  26369  dvrelog  26677  logcn  26687  logccv  26703  ppiub  27243  lgsquadlem1  27419  lgsquadlem2  27420  addsqrexnreu  27481  addsqnreup  27482  2sqreunnlem2  27494  dirith2  27567  madefi  27981  bdayfinbndlem1  28535  usgrexmpldifpr  29403  usgrexmplef  29404  disjxwwlksn  30048  disjxwwlkn  30057  nvrel  30749  phrel  30962  bnrel  31014  hlrel  31037  pjnormi  31868  lnopunilem1  32157  lnophmlem1  32163  xrge0infssd  32911  infxrge0lb  32914  infxrge0glb  32915  infxrge0gelb  32916  ssnnssfz  32937  xrge0iifiso  34191  omsf  34552  oms0  34553  omssubaddlem  34555  omssubadd  34556  oddpwdc  34610  rpsqrtcn  34849  bnj1023  35038  bnj1109  35044  erdszelem4  35497  erdszelem8  35501  gonan0  35695  2thALT  35987  supfz  36032  inffz  36033  trer  36629  fneer  36666  naim1i  36704  naim2i  36705  nmotru  36721  onpsstopbas  36743  bj-mp2c  36931  bj-mp2d  36932  bj-bijust00  36973  bj-almp  37007  bj-axseprep  37512  iccioo01  37774  pibt2  37864  wl-equsal1i  38000  wl-sbcom2d  38017  poimirlem25  38097  poimirlem26  38098  mblfinlem1  38109  incsequz2  38201  cncfres  38217  heiborlem3  38265  diclspsn  41771  dih1dimatlem  41906  rencldnfilem  43350  pellexlem4  43362  pellexlem5  43363  ttac  43566  idomsubgmo  43723  areaquad  43746  frege102  44494  lhe4.4ex1a  44858  eel0000  45248  eel00001  45249  eel00000  45250  e000  45295  e00  45296  wffr  45490  modelaxreplem1  45507  nregmodellem  45545  fzisoeu  45832  resincncf  46402  nthrucw  47415  aiota0def  47643  fvmptrabdm  47840  fmtnoinf  48098  gricrel  48494  grlicrel  48581  usgrexmpl1lem  48596  usgrexmpl2lem  48601  usgrexmpl2nb0  48606  usgrexmpl2nb1  48607  usgrexmpl2nb2  48608  usgrexmpl2nb3  48609  usgrexmpl2nb4  48610  usgrexmpl2nb5  48611  gpgprismgr4cycllem2  48671  gpg5ngric  48703  ssnn0ssfz  48924  zlmodzxzldeplem  49073  tposideq  49462