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  2658  barbarilem  2661  festino  2667  baroco  2669  darapti  2677  sstri  3947  0disj  5088  disjx0  5090  opthhausdorff  5464  relres  5960  cnvdif  6096  difxp  6117  funopab4  6523  fun0  6551  omsinds  7827  frxp3  8091  reltpos  8171  tpos0  8196  oaabs2  8574  swoer  8663  xpider  8722  sbthcl  9023  elirrvOLD  9509  unctb  10117  fin1a2lem12  10324  axcc2lem  10349  axcclem  10370  brdom3  10441  brdom5  10442  brdom4  10443  pwcfsdom  10496  smobeth  10499  pwxpndom2  10578  pwdjundom  10580  gchac  10594  wunex3  10654  inar1  10688  gruina  10731  ltsopi  10801  recmulnq  10877  prcdnq  10906  ltrel  11196  lerel  11198  suprfinzcl  12608  cnexALT  12905  dfle2  13067  dflt2  13068  uzrdg0i  13884  ltwefz  13888  fzennn  13893  faclbnd4lem1  14218  hashsslei  14351  0csh0  14717  isercolllem1  15590  zsum  15643  sum0  15646  znnen  16139  qnnen  16140  rpnnen  16154  ruc  16170  nthruc  16179  nthruz  16180  phicl2  16697  relfull  17835  relfth  17836  gicer  19174  oppglsm  19539  efgrelexlemb  19647  isunit  20276  xrsnsgrp  21332  pjpm  21633  1stcfb  23348  2ndc1stc  23354  2ndcctbss  23358  2ndcdisj2  23360  2ndcsep  23362  hmpher  23687  met1stc  24425  re2ndc  24705  iccpnfhmeo  24859  xrhmeo  24860  xrcmp  24862  xrconn  24863  dyadmbl  25517  opnmblALT  25520  vitalilem2  25526  vitalilem3  25527  vitali  25530  mbfimaopnlem  25572  mbfsup  25581  dgrval  26149  dgrcl  26154  dgrub  26155  dgrlb  26157  aannenlem3  26254  dvrelog  26562  logcn  26572  logccv  26588  ppiub  27131  lgsquadlem1  27307  lgsquadlem2  27308  addsqrexnreu  27369  addsqnreup  27370  2sqreunnlem2  27382  dirith2  27455  madefi  27845  usgrexmpldifpr  29221  usgrexmplef  29222  disjxwwlksn  29867  disjxwwlkn  29876  nvrel  30564  phrel  30777  bnrel  30829  hlrel  30852  pjnormi  31683  lnopunilem1  31972  lnophmlem1  31978  xrge0infssd  32717  infxrge0lb  32720  infxrge0glb  32721  infxrge0gelb  32722  ssnnssfz  32743  xrge0iifiso  33901  omsf  34263  oms0  34264  omssubaddlem  34266  omssubadd  34267  oddpwdc  34321  rpsqrtcn  34560  bnj1023  34746  bnj1109  34752  erdszelem4  35166  erdszelem8  35170  gonan0  35364  2thALT  35656  supfz  35701  inffz  35702  trer  36289  fneer  36326  naim1i  36364  naim2i  36365  nmotru  36381  onpsstopbas  36403  bj-mp2c  36513  bj-mp2d  36514  bj-bijust00  36550  bj-cbvalim  36618  bj-cbvexim  36619  bj-cbvalimi  36620  bj-cbveximi  36621  iccioo01  37300  pibt2  37390  wl-equsal1i  37517  wl-sbcom2d  37534  poimirlem25  37624  poimirlem26  37625  mblfinlem1  37636  incsequz2  37728  cncfres  37744  heiborlem3  37792  diclspsn  41173  dih1dimatlem  41308  rencldnfilem  42793  pellexlem4  42805  pellexlem5  42806  ttac  43009  idomsubgmo  43166  areaquad  43189  frege102  43938  lhe4.4ex1a  44302  eel0000  44693  eel00001  44694  eel00000  44695  e000  44740  e00  44741  wffr  44935  modelaxreplem1  44952  nregmodellem  44990  fzisoeu  45282  resincncf  45857  aiota0def  47081  fvmptrabdm  47278  fmtnoinf  47521  gricrel  47903  grlicrel  47982  usgrexmpl1lem  47996  usgrexmpl2lem  48001  usgrexmpl2nb0  48006  usgrexmpl2nb1  48007  usgrexmpl2nb2  48008  usgrexmpl2nb3  48009  usgrexmpl2nb4  48010  usgrexmpl2nb5  48011  gpgprismgr4cycllem2  48070  gpg5ngric  48102  ssnn0ssfz  48321  zlmodzxzldeplem  48471  tposideq  48860