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  198  imbi12i  339  pm3.2i  470  minimp-sylsimp  1552  minimp-ax2c  1554  minimp-ax2  1555  minimp-pm2.43  1556  sbcom2  2433  sstri  3577  0disj  4575  disjx0  4577  relres  5346  cnvdif  5458  difxp  5477  funopab4  5839  fun0  5868  fvsn  6351  omsinds  6976  reltpos  7244  tpostpos  7259  tpos0  7269  oaabs2  7612  swoer  7659  xpider  7705  erinxp  7708  sbthcl  7967  php  8029  elirrv  8387  inf0  8401  unctb  8910  fin1a2lem12  9116  axcc2lem  9141  axcclem  9162  brdom3  9231  brdom5  9232  brdom4  9233  pwcfsdom  9284  smobeth  9287  fpwwe2lem8  9338  fpwwe2lem9  9339  fpwwe2lem12  9342  pwxpndom2  9366  pwcdandom  9368  gchac  9382  wunex3  9442  inar1  9476  gruina  9519  ltsopi  9589  recmulnq  9665  prcdnq  9694  ltrel  9979  lerel  9981  suprfinzcl  11368  cnexALT  11704  dfle2  11856  dflt2  11857  uzrdg0i  12620  ltwefz  12624  fzennn  12629  faclbnd4lem1  12942  hashsslei  13073  0csh0  13390  isercolllem1  14243  zsum  14296  sum0  14299  znnen  14780  qnnen  14781  rpnnen  14795  ruc  14811  nthruc  14819  nthruz  14820  phicl2  15311  pwsle  15975  xpsc0  16043  xpsc1  16044  relfull  16391  relfth  16392  gicer  17541  gicerOLD  17542  oppglsm  17880  efgrelexlemb  17986  isunit  18480  opsrtoslem2  19306  xrsnsgrp  19601  pjpm  19871  1stcfb  21058  2ndc1stc  21064  2ndcctbss  21068  2ndcdisj2  21070  2ndcsep  21072  hmpher  21397  met1stc  22136  re2ndc  22412  iccpnfhmeo  22552  xrhmeo  22553  xrcmp  22555  xrcon  22556  dyadmbl  23174  opnmblALT  23177  vitalilem2  23184  vitalilem3  23185  vitali  23188  mbfimaopnlem  23228  mbfsup  23237  dgrval  23788  dgrcl  23793  dgrub  23794  dgrlb  23796  aannenlem3  23889  dvrelog  24183  logcn  24193  logccv  24209  logblog  24330  ppiub  24729  lgsquadlem1  24905  lgsquadlem2  24906  dirith2  25017  usgraexmpldifpr  25928  usgraexmplef  25929  disjxwwlks  26264  disjxwwlkn  26273  konigsberg  26514  nvrel  26841  phrel  27054  bnrel  27107  hlrel  27130  pjnormi  27964  lnopunilem1  28253  lnophmlem1  28259  xrge0infssd  28916  infxrge0lb  28919  infxrge0glb  28920  infxrge0gelb  28921  ssnnssfz  28937  xrge0iifiso  29309  omsf  29685  oms0  29686  omssubaddlem  29688  omssubadd  29689  oddpwdc  29743  bnj1023  30105  bnj1109  30111  erdszelem4  30430  erdszelem8  30434  supfz  30866  inffz  30867  inffzOLD  30868  elrn3  30906  trer  31480  fneer  31518  naim1i  31556  naim2i  31557  mont  31578  onpsstopbas  31599  bj-mp2c  31701  bj-mp2d  31702  bj-currypeirce  31714  wl-equsal1i  32508  wl-sbcom2d  32523  poimirlem25  32604  poimirlem26  32605  mblfinlem1  32616  incsequz2  32715  cncfres  32734  heiborlem3  32782  diclspsn  35501  dih1dimatlem  35636  rencldnfilem  36402  pellexlem4  36414  pellexlem5  36415  ttac  36621  idomsubgmo  36795  areaquad  36821  frege102  37279  lhe4.4ex1a  37550  eel0001  37966  eel0000  37967  eel00001  37969  eel00000  37970  e000  38015  e00  38016  fzisoeu  38455  resincncf  38760  fmtnoinf  39986  disjxwwlksn  41110  av-disjxwwlkn  41119  ssnn0ssfz  41920  zlmodzxzldeplem  42081