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  201  imbi12i  342  pm3.2i  464  minimp-syllsimp  1735  minimp-ax2c  1737  minimp-ax2  1738  minimp-pm2.43  1739  sbcom2OLD  2579  darii  2748  barbarilem  2751  festino  2759  baroco  2761  darapti  2773  sstri  3836  0disj  4868  disjx0  4870  opthhausdorff  5205  relres  5666  cnvdif  5784  difxp  5803  funopab4  6164  fun0  6191  fvsnOLD  6705  omsinds  7350  reltpos  7627  tpostpos  7642  tpos0  7652  oaabs2  7997  swoer  8044  xpider  8088  sbthcl  8357  php  8419  elirrv  8777  inf0  8802  unctb  9349  fin1a2lem12  9555  axcc2lem  9580  axcclem  9601  brdom3  9672  brdom5  9673  brdom4  9674  pwcfsdom  9727  smobeth  9730  pwxpndom2  9809  pwcdandom  9811  gchac  9825  wunex3  9885  inar1  9919  gruina  9962  ltsopi  10032  recmulnq  10108  prcdnq  10137  ltrel  10426  lerel  10428  suprfinzcl  11827  cnexALT  12115  dfle2  12273  dflt2  12274  uzrdg0i  13060  ltwefz  13064  fzennn  13069  faclbnd4lem1  13380  hashsslei  13509  0csh0  13920  0csh0OLD  13921  isercolllem1  14779  zsum  14833  sum0  14836  znnen  15322  qnnen  15323  rpnnen  15337  ruc  15353  nthruc  15362  nthruz  15363  phicl2  15851  xpsc0  16580  xpsc1  16581  relfull  16927  relfth  16928  gicer  18076  oppglsm  18415  efgrelexlemb  18523  isunit  19018  opsrtoslem2  19852  xrsnsgrp  20149  pjpm  20422  1stcfb  21626  2ndc1stc  21632  2ndcctbss  21636  2ndcdisj2  21638  2ndcsep  21640  hmpher  21965  met1stc  22703  re2ndc  22981  iccpnfhmeo  23121  xrhmeo  23122  xrcmp  23124  xrconn  23125  dyadmbl  23773  opnmblALT  23776  vitalilem2  23782  vitalilem3  23783  vitali  23786  mbfimaopnlem  23828  mbfsup  23837  dgrval  24390  dgrcl  24395  dgrub  24396  dgrlb  24398  aannenlem3  24491  dvrelog  24789  logcn  24799  logccv  24815  logblog  24939  ppiub  25349  lgsquadlem1  25525  lgsquadlem2  25526  dirith2  25637  usgrexmpldifpr  26562  usgrexmplef  26563  disjxwwlksn  27232  disjxwwlksnOLD  27233  disjxwwlkn  27247  disjxwwlknOLD  27248  nvrel  28008  phrel  28221  bnrel  28274  hlrel  28297  pjnormi  29131  lnopunilem1  29420  lnophmlem1  29426  xrge0infssd  30069  infxrge0lb  30072  infxrge0glb  30073  infxrge0gelb  30074  ssnnssfz  30092  xrge0iifiso  30522  omsf  30899  oms0  30900  omssubaddlem  30902  omssubadd  30903  oddpwdc  30957  rpsqrtcn  31216  bnj1023  31393  bnj1109  31399  erdszelem4  31718  erdszelem8  31722  supfz  32152  inffz  32153  elrn3  32190  trer  32844  fneer  32881  naim1i  32919  naim2i  32920  nmotru  32936  onpsstopbas  32957  bj-mp2c  33058  bj-mp2d  33059  bj-currypeirce  33069  bj-bijust00  33085  bj-cbvalim  33145  bj-cbvexim  33146  bj-cbvalimi  33147  bj-cbveximi  33148  wl-equsal1i  33868  wl-sbcom2d  33883  poimirlem25  33973  poimirlem26  33974  mblfinlem1  33985  incsequz2  34082  cncfres  34101  heiborlem3  34149  diclspsn  37264  dih1dimatlem  37399  rencldnfilem  38223  pellexlem4  38235  pellexlem5  38236  ttac  38441  idomsubgmo  38614  areaquad  38639  frege102  39094  lhe4.4ex1a  39363  eel0001  39768  eel0000  39769  eel00001  39770  eel00000  39771  e000  39816  e00  39817  fzisoeu  40306  resincncf  40877  aiota0def  41985  fvmptrabdm  42190  fmtnoinf  42292  ssnn0ssfz  42988  zlmodzxzldeplem  43148