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  208  imbi12i  351  pm3.2i  472  minimp-syllsimp  1625  minimp-ax2c  1627  minimp-ax2  1628  minimp-pm2.43  1629  darii  2661  barbarilem  2664  festino  2670  baroco  2672  darapti  2680  sstri  3992  0disj  5141  disjx0  5143  opthhausdorff  5518  relres  6011  cnvdif  6144  difxp  6164  funopab4  6586  fun0  6614  omsinds  7876  omsindsOLD  7877  frxp3  8137  reltpos  8216  tpos0  8241  oaabs2  8648  swoer  8733  xpider  8782  sbthcl  9095  phpOLD  9222  elirrv  9591  unctb  10200  fin1a2lem12  10406  axcc2lem  10431  axcclem  10452  brdom3  10523  brdom5  10524  brdom4  10525  pwcfsdom  10578  smobeth  10581  pwxpndom2  10660  pwdjundom  10662  gchac  10676  wunex3  10736  inar1  10770  gruina  10813  ltsopi  10883  recmulnq  10959  prcdnq  10988  ltrel  11276  lerel  11278  suprfinzcl  12676  cnexALT  12970  dfle2  13126  dflt2  13127  uzrdg0i  13924  ltwefz  13928  fzennn  13933  faclbnd4lem1  14253  hashsslei  14386  0csh0  14743  isercolllem1  15611  zsum  15664  sum0  15667  znnen  16155  qnnen  16156  rpnnen  16170  ruc  16186  nthruc  16195  nthruz  16196  phicl2  16701  relfull  17859  relfth  17860  gicer  19150  oppglsm  19510  efgrelexlemb  19618  isunit  20187  xrsnsgrp  20981  pjpm  21263  1stcfb  22949  2ndc1stc  22955  2ndcctbss  22959  2ndcdisj2  22961  2ndcsep  22963  hmpher  23288  met1stc  24030  re2ndc  24317  iccpnfhmeo  24461  xrhmeo  24462  xrcmp  24464  xrconn  24465  dyadmbl  25117  opnmblALT  25120  vitalilem2  25126  vitalilem3  25127  vitali  25130  mbfimaopnlem  25172  mbfsup  25181  dgrval  25742  dgrcl  25747  dgrub  25748  dgrlb  25750  aannenlem3  25843  dvrelog  26145  logcn  26155  logccv  26171  ppiub  26707  lgsquadlem1  26883  lgsquadlem2  26884  addsqrexnreu  26945  addsqnreup  26946  2sqreunnlem2  26958  dirith2  27031  usgrexmpldifpr  28515  usgrexmplef  28516  disjxwwlksn  29158  disjxwwlkn  29167  nvrel  29855  phrel  30068  bnrel  30120  hlrel  30143  pjnormi  30974  lnopunilem1  31263  lnophmlem1  31269  xrge0infssd  31974  infxrge0lb  31977  infxrge0glb  31978  infxrge0gelb  31979  ssnnssfz  31998  xrge0iifiso  32915  omsf  33295  oms0  33296  omssubaddlem  33298  omssubadd  33299  oddpwdc  33353  rpsqrtcn  33605  bnj1023  33791  bnj1109  33797  erdszelem4  34185  erdszelem8  34189  gonan0  34383  supfz  34698  inffz  34699  trer  35201  fneer  35238  naim1i  35276  naim2i  35277  nmotru  35293  onpsstopbas  35315  bj-mp2c  35416  bj-mp2d  35417  bj-bijust00  35454  bj-cbvalim  35522  bj-cbvexim  35523  bj-cbvalimi  35524  bj-cbveximi  35525  iccioo01  36208  pibt2  36298  wl-equsal1i  36412  wl-sbcom2d  36426  poimirlem25  36513  poimirlem26  36514  mblfinlem1  36525  incsequz2  36617  cncfres  36633  heiborlem3  36681  diclspsn  40065  dih1dimatlem  40200  rencldnfilem  41558  pellexlem4  41570  pellexlem5  41571  ttac  41775  idomsubgmo  41940  areaquad  41965  frege102  42716  lhe4.4ex1a  43088  eel0000  43481  eel00001  43482  eel00000  43483  e000  43528  e00  43529  fzisoeu  44010  resincncf  44591  aiota0def  45804  fvmptrabdm  46001  fmtnoinf  46204  ssnn0ssfz  47025  zlmodzxzldeplem  47179