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  2695  barbarilem  2698  festino  2704  baroco  2706  darapti  2714  sstri  3949  0disj  5105  disjx0  5107  opthhausdorff  5503  relres  6007  cnvdif  6143  difxp  6164  funopab4  6577  fun0  6605  omsinds  7885  frxp3  8149  reltpos  8229  tpos0  8254  oaabs2  8637  swoer  8728  xpider  8788  sbthcl  9089  elirrvOLDOLD  9563  unctb  10198  fin1a2lem12  10405  axcc2lem  10430  axcclem  10451  brdom3  10522  brdom5  10523  brdom4  10524  pwcfsdom  10578  smobeth  10581  pwxpndom2  10660  pwdjundom  10662  gchac  10676  wunex3  10736  inar1  10770  gruina  10813  ltsopi  10883  recmulnq  10959  prcdnq  10988  ltrel  11281  lerel  11283  suprfinzcl  12720  cnexALT  13020  dfle2  13182  dflt2  13183  uzrdg0i  14006  ltwefz  14010  fzennn  14015  faclbnd4lem1  14340  hashsslei  14474  0csh0  14841  isercolllem1  15727  zsum  15780  sum0  15783  znnen  16278  qnnen  16279  rpnnen  16293  ruc  16309  nthruc  16318  nthruz  16319  phicl2  16837  relfull  17977  relfth  17978  gicer  19357  oppglsm  19722  efgrelexlemb  19830  isunit  20466  ricrel  20607  xrsnsgrp  21573  pjpm  21873  1stcfb  23617  2ndc1stc  23623  2ndcctbss  23627  2ndcdisj2  23629  2ndcsep  23631  hmpher  23956  met1stc  24693  re2ndc  24973  iccpnfhmeo  25119  xrhmeo  25120  xrcmp  25122  xrconn  25123  dyadmbl  25774  opnmblALT  25777  vitalilem2  25783  vitalilem3  25784  vitali  25787  mbfimaopnlem  25829  mbfsup  25838  dgrval  26400  dgrcl  26405  dgrub  26406  dgrlb  26408  aannenlem3  26508  dvrelog  26817  logcn  26827  logccv  26843  ppiub  27383  lgsquadlem1  27559  lgsquadlem2  27560  addsqrexnreu  27621  addsqnreup  27622  2sqreunnlem2  27634  dirith2  27707  madefi  28121  bdayfinbndlem1  28675  usgrexmpldifpr  29623  usgrexmplef  29624  disjxwwlksn  30268  disjxwwlkn  30277  nvrel  30969  phrel  31182  bnrel  31234  hlrel  31257  pjnormi  32088  lnopunilem1  32377  lnophmlem1  32383  xrge0infssd  33121  infxrge0lb  33124  infxrge0glb  33125  infxrge0gelb  33126  ssnnssfz  33147  xrge0iifiso  34338  omsf  34699  oms0  34700  omssubaddlem  34702  omssubadd  34703  oddpwdc  34757  rpsqrtcn  34993  bnj1023  35182  bnj1109  35188  erdszelem4  35698  erdszelem8  35702  gonan0  35896  2thALT  36188  supfz  36233  inffz  36234  trer  36859  fneer  36896  naim1i  36934  naim2i  36935  nmotru  36951  onpsstopbas  36973  bj-mp2c  37161  bj-mp2d  37162  bj-bijust00  37202  bj-almp  37236  bj-axseprep  37743  iccioo01  38005  pibt2  38095  wl-equsal1i  38231  wl-sbcom2d  38248  poimirlem25  38328  poimirlem26  38329  mblfinlem1  38340  incsequz2  38432  cncfres  38448  heiborlem3  38496  diclspsn  42000  dih1dimatlem  42135  rencldnfilem  43579  pellexlem4  43591  pellexlem5  43592  ttac  43795  idomsubgmo  43952  areaquad  43975  frege102  44723  lhe4.4ex1a  45071  eel0000  45460  eel00001  45461  eel00000  45462  e000  45507  e00  45508  wffr  45702  modelaxreplem1  45719  nregmodellem  45757  fzisoeu  46051  resincncf  46621  nthrucw  47639  aiota0def  47865  fvmptrabdm  48062  fmtnoinf  48320  gricrel  48716  grlicrel  48803  usgrexmpl1lem  48818  usgrexmpl2lem  48823  usgrexmpl2nb0  48828  usgrexmpl2nb1  48829  usgrexmpl2nb2  48830  usgrexmpl2nb3  48831  usgrexmpl2nb4  48832  usgrexmpl2nb5  48833  gpgprismgr4cycllem2  48893  gpg5ngric  48925  ssnn0ssfz  49161  zlmodzxzldeplem  49310  tposideq  49698