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  471  minimp-syllsimp  1625  minimp-ax2c  1627  minimp-ax2  1628  minimp-pm2.43  1629  darii  2666  barbarilem  2669  festino  2675  baroco  2677  darapti  2685  sstri  3930  0disj  5066  disjx0  5068  opthhausdorff  5431  relres  5920  cnvdif  6047  difxp  6067  funopab4  6471  fun0  6499  omsinds  7733  omsindsOLD  7734  reltpos  8047  tpos0  8072  oaabs2  8479  swoer  8528  xpider  8577  sbthcl  8882  phpOLD  9005  elirrv  9355  unctb  9961  fin1a2lem12  10167  axcc2lem  10192  axcclem  10213  brdom3  10284  brdom5  10285  brdom4  10286  pwcfsdom  10339  smobeth  10342  pwxpndom2  10421  pwdjundom  10423  gchac  10437  wunex3  10497  inar1  10531  gruina  10574  ltsopi  10644  recmulnq  10720  prcdnq  10749  ltrel  11037  lerel  11039  suprfinzcl  12436  cnexALT  12726  dfle2  12881  dflt2  12882  uzrdg0i  13679  ltwefz  13683  fzennn  13688  faclbnd4lem1  14007  hashsslei  14141  0csh0  14506  isercolllem1  15376  zsum  15430  sum0  15433  znnen  15921  qnnen  15922  rpnnen  15936  ruc  15952  nthruc  15961  nthruz  15962  phicl2  16469  relfull  17624  relfth  17625  gicer  18892  oppglsm  19247  efgrelexlemb  19356  isunit  19899  xrsnsgrp  20634  pjpm  20915  1stcfb  22596  2ndc1stc  22602  2ndcctbss  22606  2ndcdisj2  22608  2ndcsep  22610  hmpher  22935  met1stc  23677  re2ndc  23964  iccpnfhmeo  24108  xrhmeo  24109  xrcmp  24111  xrconn  24112  dyadmbl  24764  opnmblALT  24767  vitalilem2  24773  vitalilem3  24774  vitali  24777  mbfimaopnlem  24819  mbfsup  24828  dgrval  25389  dgrcl  25394  dgrub  25395  dgrlb  25397  aannenlem3  25490  dvrelog  25792  logcn  25802  logccv  25818  ppiub  26352  lgsquadlem1  26528  lgsquadlem2  26529  addsqrexnreu  26590  addsqnreup  26591  2sqreunnlem2  26603  dirith2  26676  usgrexmpldifpr  27625  usgrexmplef  27626  disjxwwlksn  28269  disjxwwlkn  28278  nvrel  28964  phrel  29177  bnrel  29229  hlrel  29252  pjnormi  30083  lnopunilem1  30372  lnophmlem1  30378  xrge0infssd  31084  infxrge0lb  31087  infxrge0glb  31088  infxrge0gelb  31089  ssnnssfz  31108  xrge0iifiso  31885  omsf  32263  oms0  32264  omssubaddlem  32266  omssubadd  32267  oddpwdc  32321  rpsqrtcn  32573  bnj1023  32760  bnj1109  32766  erdszelem4  33156  erdszelem8  33160  gonan0  33354  supfz  33694  inffz  33695  trer  34505  fneer  34542  naim1i  34580  naim2i  34581  nmotru  34597  onpsstopbas  34619  bj-mp2c  34720  bj-mp2d  34721  bj-bijust00  34758  bj-cbvalim  34826  bj-cbvexim  34827  bj-cbvalimi  34828  bj-cbveximi  34829  iccioo01  35498  pibt2  35588  wl-equsal1i  35702  wl-sbcom2d  35716  poimirlem25  35802  poimirlem26  35803  mblfinlem1  35814  incsequz2  35907  cncfres  35923  heiborlem3  35971  diclspsn  39208  dih1dimatlem  39343  rencldnfilem  40642  pellexlem4  40654  pellexlem5  40655  ttac  40858  idomsubgmo  41023  areaquad  41047  frege102  41573  lhe4.4ex1a  41947  eel0000  42340  eel00001  42341  eel00000  42342  e000  42387  e00  42388  fzisoeu  42839  resincncf  43416  aiota0def  44588  fvmptrabdm  44785  fmtnoinf  44988  ssnn0ssfz  45685  zlmodzxzldeplem  45839