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  2662  barbarilem  2665  festino  2671  baroco  2673  darapti  2681  sstri  3941  0disj  5088  disjx0  5090  opthhausdorff  5462  relres  5961  cnvdif  6098  difxp  6119  funopab4  6526  fun0  6554  omsinds  7826  frxp3  8090  reltpos  8170  tpos0  8195  oaabs2  8573  swoer  8662  xpider  8721  sbthcl  9022  elirrvOLD  9494  unctb  10105  fin1a2lem12  10312  axcc2lem  10337  axcclem  10358  brdom3  10429  brdom5  10430  brdom4  10431  pwcfsdom  10484  smobeth  10487  pwxpndom2  10566  pwdjundom  10568  gchac  10582  wunex3  10642  inar1  10676  gruina  10719  ltsopi  10789  recmulnq  10865  prcdnq  10894  ltrel  11184  lerel  11186  suprfinzcl  12597  cnexALT  12894  dfle2  13056  dflt2  13057  uzrdg0i  13876  ltwefz  13880  fzennn  13885  faclbnd4lem1  14210  hashsslei  14343  0csh0  14710  isercolllem1  15582  zsum  15635  sum0  15638  znnen  16131  qnnen  16132  rpnnen  16146  ruc  16162  nthruc  16171  nthruz  16172  phicl2  16689  relfull  17827  relfth  17828  gicer  19199  oppglsm  19564  efgrelexlemb  19672  isunit  20301  xrsnsgrp  21354  pjpm  21655  1stcfb  23370  2ndc1stc  23376  2ndcctbss  23380  2ndcdisj2  23382  2ndcsep  23384  hmpher  23709  met1stc  24446  re2ndc  24726  iccpnfhmeo  24880  xrhmeo  24881  xrcmp  24883  xrconn  24884  dyadmbl  25538  opnmblALT  25541  vitalilem2  25547  vitalilem3  25548  vitali  25551  mbfimaopnlem  25593  mbfsup  25602  dgrval  26170  dgrcl  26175  dgrub  26176  dgrlb  26178  aannenlem3  26275  dvrelog  26583  logcn  26593  logccv  26609  ppiub  27152  lgsquadlem1  27328  lgsquadlem2  27329  addsqrexnreu  27390  addsqnreup  27391  2sqreunnlem2  27403  dirith2  27476  madefi  27868  usgrexmpldifpr  29247  usgrexmplef  29248  disjxwwlksn  29893  disjxwwlkn  29902  nvrel  30593  phrel  30806  bnrel  30858  hlrel  30881  pjnormi  31712  lnopunilem1  32001  lnophmlem1  32007  xrge0infssd  32755  infxrge0lb  32758  infxrge0glb  32759  infxrge0gelb  32760  ssnnssfz  32781  xrge0iifiso  33959  omsf  34320  oms0  34321  omssubaddlem  34323  omssubadd  34324  oddpwdc  34378  rpsqrtcn  34617  bnj1023  34803  bnj1109  34809  erdszelem4  35249  erdszelem8  35253  gonan0  35447  2thALT  35739  supfz  35784  inffz  35785  trer  36371  fneer  36408  naim1i  36446  naim2i  36447  nmotru  36463  onpsstopbas  36485  bj-mp2c  36595  bj-mp2d  36596  bj-bijust00  36632  bj-cbvalim  36700  bj-cbvexim  36701  bj-cbvalimi  36702  bj-cbveximi  36703  iccioo01  37382  pibt2  37472  wl-equsal1i  37599  wl-sbcom2d  37616  poimirlem25  37695  poimirlem26  37696  mblfinlem1  37707  incsequz2  37799  cncfres  37815  heiborlem3  37863  diclspsn  41303  dih1dimatlem  41438  rencldnfilem  42927  pellexlem4  42939  pellexlem5  42940  ttac  43143  idomsubgmo  43300  areaquad  43323  frege102  44072  lhe4.4ex1a  44436  eel0000  44826  eel00001  44827  eel00000  44828  e000  44873  e00  44874  wffr  45068  modelaxreplem1  45085  nregmodellem  45123  fzisoeu  45415  resincncf  45987  nthrucw  46998  aiota0def  47210  fvmptrabdm  47407  fmtnoinf  47650  gricrel  48033  grlicrel  48120  usgrexmpl1lem  48135  usgrexmpl2lem  48140  usgrexmpl2nb0  48145  usgrexmpl2nb1  48146  usgrexmpl2nb2  48147  usgrexmpl2nb3  48148  usgrexmpl2nb4  48149  usgrexmpl2nb5  48150  gpgprismgr4cycllem2  48210  gpg5ngric  48242  ssnn0ssfz  48463  zlmodzxzldeplem  48613  tposideq  49002