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  2690  barbarilem  2693  festino  2699  baroco  2701  darapti  2709  sstri  3940  0disj  5096  disjx0  5098  opthhausdorff  5490  relres  5996  cnvdif  6132  difxp  6154  funopab4  6569  fun0  6597  omsinds  7887  frxp3  8152  reltpos  8232  tpos0  8257  oaabs2  8642  swoer  8733  xpider  8793  sbthcl  9102  elirrvOLDOLD  9577  unctb  10263  fin1a2lem12  10470  axcc2lem  10495  axcclem  10516  brdom3  10588  brdom5  10589  brdom4  10590  pwcfsdom  10649  smobeth  10652  pwxpndom2  10731  pwdjundom  10733  gchac  10747  wunex3  10807  inar1  10841  gruina  10884  ltsopi  10954  recmulnq  11030  prcdnq  11059  ltrel  11352  lerel  11354  suprfinzcl  12794  cnexALT  13095  dfle2  13257  dflt2  13258  uzrdg0i  14082  ltwefz  14086  fzennn  14091  faclbnd4lem1  14417  hashsslei  14551  0csh0  14924  isercolllem1  15812  zsum  15864  sum0  15867  znnen  16360  qnnen  16361  rpnnen  16375  ruc  16391  nthruc  16400  nthruz  16401  phicl2  16925  relfull  18065  relfth  18066  gicer  19471  oppglsm  19836  efgrelexlemb  19944  isunit  20583  ricrel  20724  xrsnsgrp  21694  pjpm  21994  1stcfb  23743  2ndc1stc  23749  2ndcctbss  23754  2ndcdisj2  23756  2ndcsep  23758  hmpher  24083  met1stc  24820  re2ndc  25100  iccpnfhmeo  25246  xrhmeo  25247  xrcmp  25249  xrconn  25250  dyadmbl  25901  opnmblALT  25904  vitalilem2  25910  vitalilem3  25911  vitali  25914  mbfimaopnlem  25956  mbfsup  25965  dgrval  26527  dgrcl  26532  dgrub  26533  dgrlb  26535  aannenlem3  26639  dvrelog  26947  logcn  26957  logccv  26973  ppiub  27513  lgsquadlem1  27689  lgsquadlem2  27690  addsqrexnreu  27751  addsqnreup  27752  2sqreunnlem2  27764  dirith2  27837  bdayfinbndlem1  28835  usgrexmpldifpr  29821  usgrexmplef  29822  disjxwwlksn  30475  disjxwwlkn  30484  nvrel  31186  phrel  31399  bnrel  31451  hlrel  31474  pjnormi  32305  lnopunilem1  32594  lnophmlem1  32600  xrge0infssd  33335  infxrge0lb  33338  infxrge0glb  33339  infxrge0gelb  33340  ssnnssfz  33361  xrge0iifiso  34549  omsf  34911  oms0  34912  omssubaddlem  34914  omssubadd  34915  oddpwdc  34969  rpsqrtcn  35205  bnj1023  35394  bnj1109  35400  erdszelem4  35928  erdszelem8  35932  gonan0  36126  2thALT  36418  supfz  36463  inffz  36464  trer  37074  fneer  37111  naim1i  37149  naim2i  37150  nmotru  37166  onpsstopbas  37188  bj-mp2c  37376  bj-mp2d  37377  bj-bijust00  37417  bj-almp  37451  bj-axseprep  37958  iccioo01  38218  pibt2  38308  wl-equsal1i  38444  wl-sbcom2d  38461  poimirlem25  38531  poimirlem26  38532  mblfinlem1  38543  incsequz2  38651  cncfres  38667  heiborlem3  38715  diclspsn  42219  dih1dimatlem  42354  rencldnfilem  43780  pellexlem4  43792  pellexlem5  43793  ttac  43996  idomsubgmo  44153  areaquad  44176  frege102  44924  lhe4.4ex1a  45272  eel0000  45661  eel00001  45662  eel00000  45663  e000  45708  e00  45709  wffr  45903  modelaxreplem1  45920  nregmodellem  45958  fzisoeu  46259  resincncf  46829  numtowerdt  47860  aiota0def  48110  fvmptrabdm  48307  fmtnoinf  48565  gricrel  48961  grlicrel  49048  usgrexmpl1lem  49063  usgrexmpl2lem  49068  usgrexmpl2nb0  49073  usgrexmpl2nb1  49074  usgrexmpl2nb2  49075  usgrexmpl2nb3  49076  usgrexmpl2nb4  49077  usgrexmpl2nb5  49078  gpgprismgr4cycllem2  49138  gpg5ngric  49170  ssnn0ssfz  49405  zlmodzxzldeplem  49554  tposideq  49940