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  212  imbi12i  353  pm3.2i  475  minimp-syllsimp  1645  minimp-ax2c  1647  minimp-ax2  1648  minimp-pm2.43  1649  darii  2694  barbarilem  2697  festino  2703  baroco  2705  darapti  2713  sstri  3948  0disj  5098  disjx0  5100  opthhausdorff  5491  relres  5995  cnvdif  6131  difxp  6153  funopab4  6562  fun0  6590  omsinds  7871  frxp3  8135  reltpos  8215  tpos0  8240  oaabs2  8623  swoer  8714  xpider  8774  sbthcl  9075  elirrvOLDOLD  9549  unctb  10175  fin1a2lem12  10383  axcc2lem  10408  axcclem  10429  brdom3  10500  brdom5  10501  brdom4  10502  pwcfsdom  10556  smobeth  10559  pwxpndom2  10638  pwdjundom  10640  gchac  10654  wunex3  10714  inar1  10748  gruina  10791  ltsopi  10861  recmulnq  10937  prcdnq  10966  ltrel  11259  lerel  11261  suprfinzcl  12701  cnexALT  13001  dfle2  13163  dflt2  13164  uzrdg0i  13986  ltwefz  13990  fzennn  13995  faclbnd4lem1  14320  hashsslei  14453  0csh0  14820  isercolllem1  15706  zsum  15759  sum0  15762  znnen  16258  qnnen  16259  rpnnen  16273  ruc  16289  nthruc  16298  nthruz  16299  phicl2  16817  relfull  17957  relfth  17958  gicer  19338  oppglsm  19703  efgrelexlemb  19811  isunit  20446  xrsnsgrp  21518  pjpm  21818  1stcfb  23563  2ndc1stc  23569  2ndcctbss  23573  2ndcdisj2  23575  2ndcsep  23577  hmpher  23902  met1stc  24639  re2ndc  24919  iccpnfhmeo  25065  xrhmeo  25066  xrcmp  25068  xrconn  25069  dyadmbl  25720  opnmblALT  25723  vitalilem2  25729  vitalilem3  25730  vitali  25733  mbfimaopnlem  25775  mbfsup  25784  dgrval  26346  dgrcl  26351  dgrub  26352  dgrlb  26354  aannenlem3  26452  dvrelog  26760  logcn  26770  logccv  26786  ppiub  27326  lgsquadlem1  27502  lgsquadlem2  27503  addsqrexnreu  27564  addsqnreup  27565  2sqreunnlem2  27577  dirith2  27650  madefi  28064  bdayfinbndlem1  28618  usgrexmpldifpr  29517  usgrexmplef  29518  disjxwwlksn  30162  disjxwwlkn  30171  nvrel  30863  phrel  31076  bnrel  31128  hlrel  31151  pjnormi  31982  lnopunilem1  32271  lnophmlem1  32277  xrge0infssd  33018  infxrge0lb  33021  infxrge0glb  33022  infxrge0gelb  33023  ssnnssfz  33044  xrge0iifiso  34242  omsf  34603  oms0  34604  omssubaddlem  34606  omssubadd  34607  oddpwdc  34661  rpsqrtcn  34897  bnj1023  35086  bnj1109  35092  erdszelem4  35557  erdszelem8  35561  gonan0  35755  2thALT  36047  supfz  36092  inffz  36093  trer  36689  fneer  36726  naim1i  36764  naim2i  36765  nmotru  36781  onpsstopbas  36803  bj-mp2c  36991  bj-mp2d  36992  bj-bijust00  37032  bj-almp  37066  bj-axseprep  37571  iccioo01  37833  pibt2  37923  wl-equsal1i  38059  wl-sbcom2d  38076  poimirlem25  38156  poimirlem26  38157  mblfinlem1  38168  incsequz2  38260  cncfres  38276  heiborlem3  38324  diclspsn  41830  dih1dimatlem  41965  rencldnfilem  43409  pellexlem4  43421  pellexlem5  43422  ttac  43625  idomsubgmo  43782  areaquad  43805  frege102  44553  lhe4.4ex1a  44903  eel0000  45293  eel00001  45294  eel00000  45295  e000  45340  e00  45341  wffr  45535  modelaxreplem1  45552  nregmodellem  45590  fzisoeu  45877  resincncf  46447  nthrucw  47460  aiota0def  47688  fvmptrabdm  47885  fmtnoinf  48143  gricrel  48539  grlicrel  48626  usgrexmpl1lem  48641  usgrexmpl2lem  48646  usgrexmpl2nb0  48651  usgrexmpl2nb1  48652  usgrexmpl2nb2  48653  usgrexmpl2nb3  48654  usgrexmpl2nb4  48655  usgrexmpl2nb5  48656  gpgprismgr4cycllem2  48716  gpg5ngric  48748  ssnn0ssfz  48980  zlmodzxzldeplem  49129  tposideq  49517