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  1622  minimp-ax2c  1624  minimp-ax2  1625  minimp-pm2.43  1626  darii  2664  barbarilem  2667  festino  2673  baroco  2675  darapti  2683  sstri  3968  0disj  5112  disjx0  5114  opthhausdorff  5492  relres  5992  cnvdif  6132  difxp  6153  funopab4  6572  fun0  6600  omsinds  7880  frxp3  8148  reltpos  8228  tpos0  8253  oaabs2  8659  swoer  8748  xpider  8800  sbthcl  9107  phpOLD  9229  elirrv  9608  unctb  10216  fin1a2lem12  10423  axcc2lem  10448  axcclem  10469  brdom3  10540  brdom5  10541  brdom4  10542  pwcfsdom  10595  smobeth  10598  pwxpndom2  10677  pwdjundom  10679  gchac  10693  wunex3  10753  inar1  10787  gruina  10830  ltsopi  10900  recmulnq  10976  prcdnq  11005  ltrel  11295  lerel  11297  suprfinzcl  12705  cnexALT  13000  dfle2  13161  dflt2  13162  uzrdg0i  13975  ltwefz  13979  fzennn  13984  faclbnd4lem1  14309  hashsslei  14442  0csh0  14809  isercolllem1  15679  zsum  15732  sum0  15735  znnen  16228  qnnen  16229  rpnnen  16243  ruc  16259  nthruc  16268  nthruz  16269  phicl2  16785  relfull  17921  relfth  17922  gicer  19258  oppglsm  19621  efgrelexlemb  19729  isunit  20331  xrsnsgrp  21368  pjpm  21666  1stcfb  23381  2ndc1stc  23387  2ndcctbss  23391  2ndcdisj2  23393  2ndcsep  23395  hmpher  23720  met1stc  24458  re2ndc  24738  iccpnfhmeo  24892  xrhmeo  24893  xrcmp  24895  xrconn  24896  dyadmbl  25551  opnmblALT  25554  vitalilem2  25560  vitalilem3  25561  vitali  25564  mbfimaopnlem  25606  mbfsup  25615  dgrval  26183  dgrcl  26188  dgrub  26189  dgrlb  26191  aannenlem3  26288  dvrelog  26596  logcn  26606  logccv  26622  ppiub  27165  lgsquadlem1  27341  lgsquadlem2  27342  addsqrexnreu  27403  addsqnreup  27404  2sqreunnlem2  27416  dirith2  27489  madefi  27867  usgrexmpldifpr  29183  usgrexmplef  29184  disjxwwlksn  29832  disjxwwlkn  29841  nvrel  30529  phrel  30742  bnrel  30794  hlrel  30817  pjnormi  31648  lnopunilem1  31937  lnophmlem1  31943  xrge0infssd  32684  infxrge0lb  32687  infxrge0glb  32688  infxrge0gelb  32689  ssnnssfz  32710  xrge0iifiso  33912  omsf  34274  oms0  34275  omssubaddlem  34277  omssubadd  34278  oddpwdc  34332  rpsqrtcn  34571  bnj1023  34757  bnj1109  34763  erdszelem4  35162  erdszelem8  35166  gonan0  35360  2thALT  35652  supfz  35692  inffz  35693  trer  36280  fneer  36317  naim1i  36355  naim2i  36356  nmotru  36372  onpsstopbas  36394  bj-mp2c  36504  bj-mp2d  36505  bj-bijust00  36541  bj-cbvalim  36609  bj-cbvexim  36610  bj-cbvalimi  36611  bj-cbveximi  36612  iccioo01  37291  pibt2  37381  wl-equsal1i  37508  wl-sbcom2d  37525  poimirlem25  37615  poimirlem26  37616  mblfinlem1  37627  incsequz2  37719  cncfres  37735  heiborlem3  37783  diclspsn  41159  dih1dimatlem  41294  rencldnfilem  42790  pellexlem4  42802  pellexlem5  42803  ttac  43007  idomsubgmo  43164  areaquad  43187  frege102  43936  lhe4.4ex1a  44301  eel0000  44692  eel00001  44693  eel00000  44694  e000  44739  e00  44740  wffr  44934  modelaxreplem1  44951  fzisoeu  45277  resincncf  45852  aiota0def  47073  fvmptrabdm  47270  fmtnoinf  47498  gricrel  47880  grlicrel  47959  usgrexmpl1lem  47973  usgrexmpl2lem  47978  usgrexmpl2nb0  47983  usgrexmpl2nb1  47984  usgrexmpl2nb2  47985  usgrexmpl2nb3  47986  usgrexmpl2nb4  47987  usgrexmpl2nb5  47988  gpgprismgr4cycllem2  48043  ssnn0ssfz  48272  zlmodzxzldeplem  48422  tposideq  48811