Theorem 4syl 19

Description: Inference chaining three syllogisms syl 17. (Contributed by BJ, 14-Jul-2018.) The use of this theorem is marked "discouraged" because it can cause the Metamath program "MM-PA> MINIMIZE_WITH *" command to have very long run times. However, feel free to use "MM-PA> MINIMIZE_WITH 4syl / OVERRIDE" if you wish. Remember to update the "discouraged" file if it gets used. (New usage is discouraged.)

Hypotheses

Ref	Expression
4syl.1	⊢ (𝜑 → 𝜓)
4syl.2	⊢ (𝜓 → 𝜒)
4syl.3	⊢ (𝜒 → 𝜃)
4syl.4	⊢ (𝜃 → 𝜏)

Assertion

Ref	Expression
4syl	⊢ (𝜑 → 𝜏)

Proof of Theorem 4syl

Step	Hyp	Ref	Expression
1		4syl.1	. . 3 ⊢ (𝜑 → 𝜓)
2		4syl.2	. . 3 ⊢ (𝜓 → 𝜒)
3		4syl.3	. . 3 ⊢ (𝜒 → 𝜃)
4	1, 2, 3	3syl 18	. 2 ⊢ (𝜑 → 𝜃)
5		4syl.4	. 2 ⊢ (𝜃 → 𝜏)
6	4, 5	syl 17	1 ⊢ (𝜑 → 𝜏)

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  aevlem  2058  eqeq1d  2733  2reu5  3717  relopabi  5762  f1ocnvfvrneq  7220  fcof1oinvd  7227  isoselem  7275  isose  7277  fnwelem  8061  tposss  8157  smoiso  8282  nneob  8571  difsnen  8972  php  9116  ordtypelem10  9413  oismo  9426  cantnflt2  9563  oemapso  9572  cantnf  9583  scott0  9779  tskwe  9843  infxpenlem  9904  ac10ct  9925  acndom  9942  dfac12lem2  10036  dfac12r  10038  pwdjudom  10106  ackbij1lem15  10124  ackbij2lem2  10130  ackbij2lem3  10131  ackbij2  10133  fin23lem22  10218  domtriomlem  10333  axdc3lem2  10342  sdomsdomcard  10451  fpwwe2lem8  10529  canthp1lem2  10544  pwfseqlem5  10554  xnn0lem1lt  13143  fzssp1  13467  fzosplitsnm1  13640  fzofzp1  13664  fzostep1  13686  fldiv4lem1div2uz2  13740  fsuppmapnn0fiublem  13897  fsuppmapnn0fiub  13898  bcm1k  14222  pfxccatpfx2  14644  revrev  14674  climuni  15459  isercolllem2  15573  isercoll  15575  serf0  15588  fsumparts  15713  hashiun  15729  isumsup2  15753  climcndslem1  15756  climcndslem2  15757  binomfallfaclem2  15947  2mulprm  16604  oddprm  16722  vdwmc  16890  prdsplusg  17362  prdsvsca  17364  imasdsval2  17420  catcone0  17593  sscpwex  17722  ssc2  17729  pmtrfv  19365  symgtrinv  19385  psgnprfval  19434  odcl2  19478  lsmmod  19588  efgsdmi  19645  gsumzinv  19858  ablfac1b  19985  pgpfac1lem1  19989  pgpfaclem2  19997  ablfaclem2  20001  ablfac  20003  srng0  20770  orngsqr  20782  orngmullt  20787  ofldtos  20789  rmodislmod  20864  znzrh2  21483  znf1o  21489  znhash  21496  znfld  21498  cygznlem3  21507  psgnevpmb  21525  ip2di  21579  mpofrlmd  21715  ascl0  21822  ascl1  21823  mpfsubrg  22039  gsumply1subr  22147  evls1gsumadd  22240  pf1subrg  22264  mpfpf1  22267  pf1mpf  22268  scmatsgrp1  22438  madutpos  22558  iscncl  23185  qtopcmap  23635  hmeores  23687  qtopf1  23732  fbssfi  23753  filssufil  23828  fmfnfmlem3  23872  clssubg  24025  tmsxms  24402  prdsxms  24446  metustfbas  24473  metuel2  24481  restmetu  24486  tngngp2  24568  nrginvrcn  24608  nmhmcn  25048  iscmet3  25221  minveclem3  25357  ovoliunlem2  25432  ismbf3d  25583  i1fd  25610  dvadd  25871  dvmul  25872  dvaddf  25873  dvco  25879  dvcof  25880  dvcnvlem  25908  dgrub  26167  plyremlem  26240  fta1lem  26243  fta1  26244  vieta1lem2  26247  plyexmo  26249  elaa  26252  ulmcau  26332  ulmdvlem3  26339  efabl  26487  relogbf  26729  ppinprm  27090  chtnprm  27092  dchrzrh1  27183  dchr1  27196  dchr1re  27202  dchrptlem1  27203  dchrpt  27206  dchrsum2  27207  dchrhash  27210  gausslemma2dlem0c  27297  gausslemma2dlem0e  27299  gausslemma2dlem0i  27303  gausslemma2dlem1a  27304  gausslemma2dlem7  27312  gausslemma2d  27313  rpvmasumlem  27426  rpvmasum2  27451  mudivsum  27469  nosepssdm  27626  nosupbnd2lem1  27655  nosupbnd2  27656  noinfbnd2lem1  27670  noetasuplem2  27674  noetasuplem3  27675  noetainflem2  27678  tgldimor  28481  f1otrg  28850  nbusgrvtxm1  29358  wlkp1lem2  29652  pthdlem1  29745  crctcshlem4  29799  crctcshwlkn0  29800  crctcshtrl  29802  wspthsnonn0vne  29896  eupth2eucrct  30195  eupthvdres  30213  eucrctshift  30221  eucrct2eupth1  30222  minvecolem3  30854  acunirnmpt2  32640  acunirnmpt2f  32641  fnpreimac  32651  symgfcoeu  33049  tocycfvres1  33077  tocycfvres2  33078  tocyc01  33085  cycpmconjslem1  33121  cycpmconjslem2  33122  archiabllem1a  33158  znfermltl  33329  qusrn  33372  ressply1invg  33530  ressply1sub  33531  ply1fermltl  33546  dimkerim  33638  fedgmullem2  33641  lvecendof1f1o  33644  evls1fldgencl  33681  algextdeglem5  33732  mdetlap  33843  locfinref  33852  ordtconnlem1  33935  pl1cn  33966  zrhunitpreima  33987  qqhnm  34001  qqhucn  34003  rrexttps  34017  ldgenpisyslem1  34174  ddemeas  34247  1stmbfm  34271  2ndmbfm  34272  omsval  34304  sitgclbn  34354  eulerpartgbij  34383  eulerpartlemgs2  34391  unveldomd  34426  probmeasb  34441  plymulx0  34558  signstres  34586  bnj1098  34793  usgrcyclgt2v  35173  subfacp1lem5  35226  erdsze2lem1  35245  cvmseu  35318  cvmliftlem11  35337  cvmlift3lem8  35368  cvmlift3lem9  35369  trer  36356  meran1  36451  lukshef-ax2  36455  ordcmp  36487  curryset  36986  currysetlem3  36989  bj-snsetex  37003  pibt2  37457  wl-nfeqfb  37576  phpreu  37650  poimirlem1  37667  poimirlem2  37668  poimirlem9  37675  poimirlem18  37684  poimirlem27  37693  poimirlem31  37697  poimirlem32  37698  mblfinlem2  37704  sdclem2  37788  ismtyhmeolem  37850  heiborlem10  37866  notornotel1  38141  mpobi123f  38208  lpssat  39058  lssatle  39060  lssat  39061  cdlemk45  40992  dia2dimlem9  41117  diblsmopel  41216  dochspss  41423  baerlem5blem2  41757  hdmap14lem4a  41916  lcmineqlem2  42069  aks6d1c1p2  42148  aks6d1c1p3  42149  hashscontpowcl  42159  hashscontpow  42161  aks6d1c4  42163  idomnnzpownz  42171  idomnnzgmulnz  42172  aks6d1c6lem3  42211  aks6d1c6lem5  42216  aks6d1c7lem1  42219  aomclem6  43098  kelac1  43102  kelac2  43104  isnumbasgrplem3  43144  proot1mul  43233  ntrclsk3  44109  neicvgel1  44158  ismnushort  44340  choicefi  45243  infleinflem1  45414  supcnvlimsup  45784  stoweidlem11  46055  stoweidlem14  46058  fourierdlem12  46163  fourierdlem48  46198  fourierdlem51  46201  fourierdlem80  46230  sssmf  46782  smfresal  46832  simpcntrab  46914  natglobalincr  46921  adh-minim  47038  afv0nbfvbi  47188  iccelpart  47470  fmtnoprmfac2lem1  47603  perfectALTVlem1  47758  bgoldbtbndlem2  47843  cznabel  48297  mgpsumz  48399  uprcl2  49227  lanrcl  49659  ranrcl  49660