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 ⊢ 𝜒

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5

This theorem is used by:  impbii  212  imbi12i  353  pm3.2i  476  minimp-syllsimp  1655  minimp-ax2c  1657  minimp-ax2  1658  minimp-pm2.43  1659  darii  2691  barbarilem  2694  festino  2700  baroco  2702  darapti  2710  sstri  3943  0disj  5100  disjx0  5102  opthhausdorff  5498  relres  6002  cnvdif  6138  difxp  6160  funopab4  6574  fun0  6602  omsinds  7887  frxp3  8153  reltpos  8233  tpos0  8258  oaabs2  8641  swoer  8732  xpider  8792  sbthcl  9101  elirrvOLDOLD  9575  unctb  10210  fin1a2lem12  10417  axcc2lem  10442  axcclem  10463  brdom3  10535  brdom5  10536  brdom4  10537  pwcfsdom  10596  smobeth  10599  pwxpndom2  10678  pwdjundom  10680  gchac  10694  wunex3  10754  inar1  10788  gruina  10831  ltsopi  10901  recmulnq  10977  prcdnq  11006  ltrel  11299  lerel  11301  suprfinzcl  12739  cnexALT  13040  dfle2  13202  dflt2  13203  uzrdg0i  14027  ltwefz  14031  fzennn  14036  faclbnd4lem1  14361  hashsslei  14495  0csh0  14868  isercolllem1  15756  zsum  15808  sum0  15811  znnen  16306  qnnen  16307  rpnnen  16321  ruc  16337  nthruc  16346  nthruz  16347  phicl2  16865  relfull  18005  relfth  18006  gicer  19410  oppglsm  19775  efgrelexlemb  19883  isunit  20520  ricrel  20661  xrsnsgrp  21627  pjpm  21927  1stcfb  23676  2ndc1stc  23682  2ndcctbss  23687  2ndcdisj2  23689  2ndcsep  23691  hmpher  24016  met1stc  24753  re2ndc  25033  iccpnfhmeo  25179  xrhmeo  25180  xrcmp  25182  xrconn  25183  dyadmbl  25834  opnmblALT  25837  vitalilem2  25843  vitalilem3  25844  vitali  25847  mbfimaopnlem  25889  mbfsup  25898  dgrval  26461  dgrcl  26466  dgrub  26467  dgrlb  26469  aannenlem3  26573  dvrelog  26882  logcn  26892  logccv  26908  ppiub  27448  lgsquadlem1  27624  lgsquadlem2  27625  addsqrexnreu  27686  addsqnreup  27687  2sqreunnlem2  27699  dirith2  27772  bdayfinbndlem1  28740  usgrexmpldifpr  29726  usgrexmplef  29727  disjxwwlksn  30380  disjxwwlkn  30389  nvrel  31091  phrel  31304  bnrel  31356  hlrel  31379  pjnormi  32210  lnopunilem1  32499  lnophmlem1  32505  xrge0infssd  33240  infxrge0lb  33243  infxrge0glb  33244  infxrge0gelb  33245  ssnnssfz  33266  xrge0iifiso  34453  omsf  34815  oms0  34816  omssubaddlem  34818  omssubadd  34819  oddpwdc  34873  rpsqrtcn  35109  bnj1023  35298  bnj1109  35304  erdszelem4  35781  erdszelem8  35785  gonan0  35979  2thALT  36271  supfz  36316  inffz  36317  trer  36943  fneer  36980  naim1i  37018  naim2i  37019  nmotru  37035  onpsstopbas  37057  bj-mp2c  37245  bj-mp2d  37246  bj-bijust00  37286  bj-almp  37320  bj-axseprep  37827  iccioo01  38089  pibt2  38179  wl-equsal1i  38315  wl-sbcom2d  38332  poimirlem25  38402  poimirlem26  38403  mblfinlem1  38414  incsequz2  38507  cncfres  38523  heiborlem3  38571  diclspsn  42075  dih1dimatlem  42210  rencldnfilem  43669  pellexlem4  43681  pellexlem5  43682  ttac  43885  idomsubgmo  44042  areaquad  44065  frege102  44813  lhe4.4ex1a  45161  eel0000  45550  eel00001  45551  eel00000  45552  e000  45597  e00  45598  wffr  45792  modelaxreplem1  45809  nregmodellem  45847  fzisoeu  46141  resincncf  46711  numtowerdt  47742  aiota0def  47992  fvmptrabdm  48189  fmtnoinf  48447  gricrel  48843  grlicrel  48930  usgrexmpl1lem  48945  usgrexmpl2lem  48950  usgrexmpl2nb0  48955  usgrexmpl2nb1  48956  usgrexmpl2nb2  48957  usgrexmpl2nb3  48958  usgrexmpl2nb4  48959  usgrexmpl2nb5  48960  gpgprismgr4cycllem2  49020  gpg5ngric  49052  ssnn0ssfz  49287  zlmodzxzldeplem  49436  tposideq  49822