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  209  imbi12i  350  pm3.2i  470  minimp-syllsimp  1623  minimp-ax2c  1625  minimp-ax2  1626  minimp-pm2.43  1627  darii  2659  barbarilem  2662  festino  2668  baroco  2670  darapti  2678  sstri  3942  0disj  5082  disjx0  5084  opthhausdorff  5455  relres  5951  cnvdif  6087  difxp  6108  funopab4  6514  fun0  6542  omsinds  7812  frxp3  8076  reltpos  8156  tpos0  8181  oaabs2  8559  swoer  8648  xpider  8707  sbthcl  9007  elirrvOLD  9479  unctb  10087  fin1a2lem12  10294  axcc2lem  10319  axcclem  10340  brdom3  10411  brdom5  10412  brdom4  10413  pwcfsdom  10466  smobeth  10469  pwxpndom2  10548  pwdjundom  10550  gchac  10564  wunex3  10624  inar1  10658  gruina  10701  ltsopi  10771  recmulnq  10847  prcdnq  10876  ltrel  11166  lerel  11168  suprfinzcl  12579  cnexALT  12876  dfle2  13038  dflt2  13039  uzrdg0i  13858  ltwefz  13862  fzennn  13867  faclbnd4lem1  14192  hashsslei  14325  0csh0  14692  isercolllem1  15564  zsum  15617  sum0  15620  znnen  16113  qnnen  16114  rpnnen  16128  ruc  16144  nthruc  16153  nthruz  16154  phicl2  16671  relfull  17809  relfth  17810  gicer  19182  oppglsm  19547  efgrelexlemb  19655  isunit  20284  xrsnsgrp  21337  pjpm  21638  1stcfb  23353  2ndc1stc  23359  2ndcctbss  23363  2ndcdisj2  23365  2ndcsep  23367  hmpher  23692  met1stc  24429  re2ndc  24709  iccpnfhmeo  24863  xrhmeo  24864  xrcmp  24866  xrconn  24867  dyadmbl  25521  opnmblALT  25524  vitalilem2  25530  vitalilem3  25531  vitali  25534  mbfimaopnlem  25576  mbfsup  25585  dgrval  26153  dgrcl  26158  dgrub  26159  dgrlb  26161  aannenlem3  26258  dvrelog  26566  logcn  26576  logccv  26592  ppiub  27135  lgsquadlem1  27311  lgsquadlem2  27312  addsqrexnreu  27373  addsqnreup  27374  2sqreunnlem2  27386  dirith2  27459  madefi  27851  usgrexmpldifpr  29229  usgrexmplef  29230  disjxwwlksn  29875  disjxwwlkn  29884  nvrel  30572  phrel  30785  bnrel  30837  hlrel  30860  pjnormi  31691  lnopunilem1  31980  lnophmlem1  31986  xrge0infssd  32734  infxrge0lb  32737  infxrge0glb  32738  infxrge0gelb  32739  ssnnssfz  32760  xrge0iifiso  33938  omsf  34299  oms0  34300  omssubaddlem  34302  omssubadd  34303  oddpwdc  34357  rpsqrtcn  34596  bnj1023  34782  bnj1109  34788  erdszelem4  35206  erdszelem8  35210  gonan0  35404  2thALT  35696  supfz  35741  inffz  35742  trer  36329  fneer  36366  naim1i  36404  naim2i  36405  nmotru  36421  onpsstopbas  36443  bj-mp2c  36553  bj-mp2d  36554  bj-bijust00  36590  bj-cbvalim  36658  bj-cbvexim  36659  bj-cbvalimi  36660  bj-cbveximi  36661  iccioo01  37340  pibt2  37430  wl-equsal1i  37557  wl-sbcom2d  37574  poimirlem25  37664  poimirlem26  37665  mblfinlem1  37676  incsequz2  37768  cncfres  37784  heiborlem3  37832  diclspsn  41212  dih1dimatlem  41347  rencldnfilem  42832  pellexlem4  42844  pellexlem5  42845  ttac  43048  idomsubgmo  43205  areaquad  43228  frege102  43977  lhe4.4ex1a  44341  eel0000  44731  eel00001  44732  eel00000  44733  e000  44778  e00  44779  wffr  44973  modelaxreplem1  44990  nregmodellem  45028  fzisoeu  45320  resincncf  45892  aiota0def  47106  fvmptrabdm  47303  fmtnoinf  47546  gricrel  47929  grlicrel  48016  usgrexmpl1lem  48031  usgrexmpl2lem  48036  usgrexmpl2nb0  48041  usgrexmpl2nb1  48042  usgrexmpl2nb2  48043  usgrexmpl2nb3  48044  usgrexmpl2nb4  48045  usgrexmpl2nb5  48046  gpgprismgr4cycllem2  48106  gpg5ngric  48138  ssnn0ssfz  48359  zlmodzxzldeplem  48509  tposideq  48898