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  353  pm3.2i  473  minimp-syllsimp  1623  minimp-ax2c  1625  minimp-ax2  1626  minimp-pm2.43  1627  darii  2750  barbarilem  2753  festino  2759  baroco  2761  darapti  2769  sstri  3978  0disj  5060  disjx0  5062  opthhausdorff  5409  relres  5884  cnvdif  6004  difxp  6023  funopab4  6394  fun0  6421  omsinds  7602  reltpos  7899  tpos0  7924  oaabs2  8274  swoer  8321  xpider  8370  sbthcl  8641  php  8703  elirrv  9062  inf0  9086  unctb  9629  fin1a2lem12  9835  axcc2lem  9860  axcclem  9881  brdom3  9952  brdom5  9953  brdom4  9954  pwcfsdom  10007  smobeth  10010  pwxpndom2  10089  pwdjundom  10091  gchac  10105  wunex3  10165  inar1  10199  gruina  10242  ltsopi  10312  recmulnq  10388  prcdnq  10417  ltrel  10705  lerel  10707  suprfinzcl  12100  cnexALT  12388  dfle2  12543  dflt2  12544  uzrdg0i  13330  ltwefz  13334  fzennn  13339  faclbnd4lem1  13656  hashsslei  13790  0csh0  14157  isercolllem1  15023  zsum  15077  sum0  15080  znnen  15567  qnnen  15568  rpnnen  15582  ruc  15598  nthruc  15607  nthruz  15608  phicl2  16107  relfull  17180  relfth  17181  gicer  18418  oppglsm  18769  efgrelexlemb  18878  isunit  19409  xrsnsgrp  20583  pjpm  20854  1stcfb  22055  2ndc1stc  22061  2ndcctbss  22065  2ndcdisj2  22067  2ndcsep  22069  hmpher  22394  met1stc  23133  re2ndc  23411  iccpnfhmeo  23551  xrhmeo  23552  xrcmp  23554  xrconn  23555  dyadmbl  24203  opnmblALT  24206  vitalilem2  24212  vitalilem3  24213  vitali  24216  mbfimaopnlem  24258  mbfsup  24267  dgrval  24820  dgrcl  24825  dgrub  24826  dgrlb  24828  aannenlem3  24921  dvrelog  25222  logcn  25232  logccv  25248  ppiub  25782  lgsquadlem1  25958  lgsquadlem2  25959  addsqrexnreu  26020  addsqnreup  26021  2sqreunnlem2  26033  dirith2  26106  usgrexmpldifpr  27042  usgrexmplef  27043  disjxwwlksn  27684  disjxwwlkn  27694  nvrel  28381  phrel  28594  bnrel  28646  hlrel  28669  pjnormi  29500  lnopunilem1  29789  lnophmlem1  29795  xrge0infssd  30487  infxrge0lb  30490  infxrge0glb  30491  infxrge0gelb  30492  ssnnssfz  30512  xrge0iifiso  31180  omsf  31556  oms0  31557  omssubaddlem  31559  omssubadd  31560  oddpwdc  31614  rpsqrtcn  31866  bnj1023  32054  bnj1109  32060  erdszelem4  32443  erdszelem8  32447  gonan0  32641  supfz  32962  inffz  32963  trer  33666  fneer  33703  naim1i  33741  naim2i  33742  nmotru  33758  onpsstopbas  33780  bj-mp2c  33881  bj-mp2d  33882  bj-bijust00  33912  bj-cbvalim  33980  bj-cbvexim  33981  bj-cbvalimi  33982  bj-cbveximi  33983  pibt2  34700  wl-equsal1i  34785  wl-sbcom2d  34799  poimirlem25  34919  poimirlem26  34920  mblfinlem1  34931  incsequz2  35026  cncfres  35045  heiborlem3  35093  diclspsn  38332  dih1dimatlem  38467  rencldnfilem  39424  pellexlem4  39436  pellexlem5  39437  ttac  39640  idomsubgmo  39805  areaquad  39830  frege102  40318  lhe4.4ex1a  40668  eel0000  41061  eel00001  41062  eel00000  41063  e000  41108  e00  41109  fzisoeu  41574  resincncf  42165  aiota0def  43301  fvmptrabdm  43499  fmtnoinf  43705  ssnn0ssfz  44404  zlmodzxzldeplem  44560