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  1620  minimp-ax2c  1622  minimp-ax2  1623  minimp-pm2.43  1624  darii  2668  barbarilem  2671  festino  2677  baroco  2679  darapti  2687  sstri  4018  0disj  5159  disjx0  5161  opthhausdorff  5536  relres  6035  cnvdif  6175  difxp  6195  funopab4  6615  fun0  6643  omsinds  7924  omsindsOLD  7925  frxp3  8192  reltpos  8272  tpos0  8297  oaabs2  8705  swoer  8794  xpider  8846  sbthcl  9161  phpOLD  9285  elirrv  9665  unctb  10273  fin1a2lem12  10480  axcc2lem  10505  axcclem  10526  brdom3  10597  brdom5  10598  brdom4  10599  pwcfsdom  10652  smobeth  10655  pwxpndom2  10734  pwdjundom  10736  gchac  10750  wunex3  10810  inar1  10844  gruina  10887  ltsopi  10957  recmulnq  11033  prcdnq  11062  ltrel  11352  lerel  11354  suprfinzcl  12757  cnexALT  13051  dfle2  13209  dflt2  13210  uzrdg0i  14010  ltwefz  14014  fzennn  14019  faclbnd4lem1  14342  hashsslei  14475  0csh0  14841  isercolllem1  15713  zsum  15766  sum0  15769  znnen  16260  qnnen  16261  rpnnen  16275  ruc  16291  nthruc  16300  nthruz  16301  phicl2  16815  relfull  17975  relfth  17976  gicer  19317  oppglsm  19684  efgrelexlemb  19792  isunit  20399  xrsnsgrp  21443  pjpm  21751  1stcfb  23474  2ndc1stc  23480  2ndcctbss  23484  2ndcdisj2  23486  2ndcsep  23488  hmpher  23813  met1stc  24555  re2ndc  24842  iccpnfhmeo  24995  xrhmeo  24996  xrcmp  24998  xrconn  24999  dyadmbl  25654  opnmblALT  25657  vitalilem2  25663  vitalilem3  25664  vitali  25667  mbfimaopnlem  25709  mbfsup  25718  dgrval  26287  dgrcl  26292  dgrub  26293  dgrlb  26295  aannenlem3  26390  dvrelog  26697  logcn  26707  logccv  26723  ppiub  27266  lgsquadlem1  27442  lgsquadlem2  27443  addsqrexnreu  27504  addsqnreup  27505  2sqreunnlem2  27517  dirith2  27590  madefi  27968  usgrexmpldifpr  29293  usgrexmplef  29294  disjxwwlksn  29937  disjxwwlkn  29946  nvrel  30634  phrel  30847  bnrel  30899  hlrel  30922  pjnormi  31753  lnopunilem1  32042  lnophmlem1  32048  xrge0infssd  32768  infxrge0lb  32771  infxrge0glb  32772  infxrge0gelb  32773  ssnnssfz  32792  xrge0iifiso  33881  omsf  34261  oms0  34262  omssubaddlem  34264  omssubadd  34265  oddpwdc  34319  rpsqrtcn  34570  bnj1023  34756  bnj1109  34762  erdszelem4  35162  erdszelem8  35166  gonan0  35360  2thALT  35652  supfz  35691  inffz  35692  trer  36282  fneer  36319  naim1i  36357  naim2i  36358  nmotru  36374  onpsstopbas  36396  bj-mp2c  36506  bj-mp2d  36507  bj-bijust00  36543  bj-cbvalim  36611  bj-cbvexim  36612  bj-cbvalimi  36613  bj-cbveximi  36614  iccioo01  37293  pibt2  37383  wl-equsal1i  37498  wl-sbcom2d  37515  poimirlem25  37605  poimirlem26  37606  mblfinlem1  37617  incsequz2  37709  cncfres  37725  heiborlem3  37773  diclspsn  41151  dih1dimatlem  41286  rencldnfilem  42776  pellexlem4  42788  pellexlem5  42789  ttac  42993  idomsubgmo  43154  areaquad  43177  frege102  43927  lhe4.4ex1a  44298  eel0000  44691  eel00001  44692  eel00000  44693  e000  44738  e00  44739  fzisoeu  45215  resincncf  45796  aiota0def  47011  fvmptrabdm  47208  fmtnoinf  47410  gricrel  47772  grlicrel  47823  usgrexmpl1lem  47836  usgrexmpl2lem  47841  usgrexmpl2nb0  47846  usgrexmpl2nb1  47847  usgrexmpl2nb2  47848  usgrexmpl2nb3  47849  usgrexmpl2nb4  47850  usgrexmpl2nb5  47851  ssnn0ssfz  48074  zlmodzxzldeplem  48227