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  2692  barbarilem  2695  festino  2701  baroco  2703  darapti  2711  sstri  3922  0disj  5099  disjx0  5101  opthhausdorff  5494  relresOLD  6008  cnvdif  6146  difxp  6167  funopab4  6597  fun0  6627  omsinds  7922  frxp3  8195  reltpos  8276  tpos0  8301  oaabs2  8686  swoer  8777  xpider  8837  sbthcl  9146  elirrvOLDOLD  9620  unctb  10309  fin1a2lem12  10516  axcc2lem  10541  axcclem  10562  brdom3  10634  brdom5  10635  brdom4  10636  pwcfsdom  10695  smobeth  10698  pwxpndom2  10777  pwdjundom  10779  gchac  10793  wunex3  10853  inar1  10887  gruina  10930  ltsopi  11000  recmulnq  11076  prcdnq  11105  ltrel  11398  lerel  11400  suprfinzcl  12840  cnexALT  13141  dfle2  13303  dflt2  13304  uzrdg0i  14129  ltwefz  14133  fzennn  14138  faclbnd4lem1  14464  hashsslei  14598  0csh0  14972  isercolllem1  15861  zsum  15913  sum0  15916  znnen  16409  qnnen  16410  rpnnen  16424  ruc  16440  nthruc  16449  nthruz  16450  phicl2  16974  relfull  18114  relfth  18115  gicer  19521  oppglsm  19886  efgrelexlemb  19994  isunit  20633  ricrel  20774  xrsnsgrp  21744  pjpm  22044  1stcfb  23793  2ndc1stc  23799  2ndcctbss  23804  2ndcdisj2  23806  2ndcsep  23808  hmpher  24133  met1stc  24870  re2ndc  25150  iccpnfhmeo  25296  xrhmeo  25297  xrcmp  25299  xrconn  25300  dyadmbl  25951  opnmblALT  25954  vitalilem2  25960  vitalilem3  25961  vitali  25964  mbfimaopnlem  26006  mbfsup  26015  dgrval  26577  dgrcl  26582  dgrub  26583  dgrlb  26585  aannenlem3  26687  dvrelog  26995  logcn  27005  logccv  27021  ppiub  27561  lgsquadlem1  27737  lgsquadlem2  27738  addsqrexnreu  27799  addsqnreup  27800  2sqreunnlem2  27812  dirith2  27885  bdayfinbndlem1  28883  usgrexmpldifpr  29869  usgrexmplef  29870  disjxwwlksn  30523  disjxwwlkn  30532  nvrel  31234  phrel  31447  bnrel  31499  hlrel  31522  pjnormi  32353  lnopunilem1  32642  lnophmlem1  32648  xrge0infssd  33423  infxrge0lb  33426  infxrge0glb  33427  infxrge0gelb  33428  ssnnssfz  33449  xrge0iifiso  34637  omsf  34998  oms0  34999  omssubaddlem  35001  omssubadd  35002  oddpwdc  35056  rpsqrtcn  35292  bnj1023  35481  bnj1109  35487  erdszelem4  36126  erdszelem8  36130  gonan0  36324  2thALT  36616  onprcr  36631  supfz  36672  inffz  36673  trer  37282  fneer  37319  naim1i  37357  naim2i  37358  nmotru  37374  onpsstopbas  37396  bj-mp2c  37584  bj-mp2d  37585  bj-bijust00  37625  bj-almp  37659  bj-axseprep  38181  iccioo01  38442  pibt2  38532  wl-equsal1i  38668  wl-sbcom2d  38685  poimirlem25  38755  poimirlem26  38756  mblfinlem1  38767  incsequz2  38875  cncfres  38891  heiborlem3  38939  diclspsn  42443  dih1dimatlem  42578  rencldnfilem  44020  pellexlem4  44032  pellexlem5  44033  ttac  44236  idomsubgmo  44387  areaquad  44410  frege102  45157  lhe4.4ex1a  45505  eel0000  45893  eel00001  45894  eel00000  45895  e000  45940  e00  45941  wffr  46146  modelaxreplem1  46163  nregmodellem  46201  hfstructwe  46234  fzisoeu  46521  resincncf  47090  numtowerdt  48121  aiota0def  48371  fvmptrabdm  48568  fmtnoinf  48826  gricrel  49222  grlicrel  49309  usgrexmpl1lem  49324  usgrexmpl2lem  49329  usgrexmpl2nb0  49334  usgrexmpl2nb1  49335  usgrexmpl2nb2  49336  usgrexmpl2nb3  49337  usgrexmpl2nb4  49338  usgrexmpl2nb5  49339  gpgprismgr4cycllem2  49399  gpg5ngric  49431  ssnn0ssfz  49666  zlmodzxzldeplem  49815  tposideq  50206