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  2076  eqeq1d  2763  2reu5  3720  relopabi  5793  f1ocnvfvrneq  7266  fcof1oinvd  7273  isoselem  7321  isose  7323  fnwelem  8106  tposss  8202  smoiso  8328  nneob  8621  difsnen  9027  php  9171  ordtypelem10  9472  oismo  9485  cantnflt2  9625  oemapso  9634  cantnf  9645  scott0  9841  tskwe  9905  infxpenlem  9966  ac10ct  9987  acndom  10004  dfac12lem2  10098  dfac12r  10100  pwdjudom  10168  ackbij1lem15  10186  ackbij2lem2  10192  ackbij2lem3  10193  ackbij2  10195  fin23lem22  10281  domtriomlem  10396  axdc3lem2  10405  sdomsdomcard  10514  fpwwe2lem8  10593  canthp1lem2  10608  pwfseqlem5  10618  xnn0lem1lt  13244  fzssp1  13569  fzosplitsnm1  13743  fzofzp1  13767  fzostep1  13789  fldiv4lem1div2uz2  13843  fsuppmapnn0fiublem  14000  fsuppmapnn0fiub  14001  bcm1k  14325  pfxccatpfx2  14747  revrev  14777  climuni  15562  isercolllem2  15676  isercoll  15678  serf0  15691  fsumparts  15817  hashiun  15833  isumsup2  15859  climcndslem1  15862  climcndslem2  15863  binomfallfaclem2  16053  2mulprm  16710  oddprm  16829  vdwmc  16997  prdsplusg  17470  prdsvsca  17472  imasdsval2  17529  catcone0  17702  sscpwex  17831  ssc2  17838  pmtrfv  19475  symgtrinv  19495  psgnprfval  19544  odcl2  19588  lsmmod  19698  efgsdmi  19755  gsumzinv  19968  ablfac1b  20095  pgpfac1lem1  20099  pgpfaclem2  20107  ablfaclem2  20111  ablfac  20113  srng0  20883  orngsqr  20895  orngmullt  20900  ofldtos  20902  rmodislmod  20977  znzrh2  21577  znf1o  21583  znhash  21590  znfld  21592  cygznlem3  21601  psgnevpmb  21619  ip2di  21673  mpofrlmd  21809  ascl0  21916  ascl1  21917  mpfsubrg  22144  gsumply1subr  22275  evls1gsumadd  22367  pf1subrg  22391  mpfpf1  22394  pf1mpf  22395  scmatsgrp1  22562  madutpos  22682  iscncl  23309  qtopcmap  23759  hmeores  23811  qtopf1  23856  fbssfi  23877  filssufil  23952  fmfnfmlem3  23996  clssubg  24149  tmsxms  24526  prdsxms  24570  metustfbas  24597  metuel2  24605  restmetu  24610  tngngp2  24692  nrginvrcn  24732  nmhmcn  25162  iscmet3  25335  minveclem3  25471  ovoliunlem2  25545  ismbf3d  25696  i1fd  25723  dvadd  25982  dvmul  25983  dvaddf  25984  dvco  25989  dvcof  25990  dvcnvlem  26018  dgrub  26274  plyremlem  26345  fta1lem  26348  fta1  26349  vieta1lem2  26352  plyexmo  26354  elaa  26357  ulmcau  26435  ulmdvlem3  26442  efabl  26592  relogbf  26833  ppinprm  27193  chtnprm  27195  dchrzrh1  27285  dchr1  27298  dchr1re  27304  dchrptlem1  27305  dchrpt  27308  dchrsum2  27309  dchrhash  27312  gausslemma2dlem0c  27399  gausslemma2dlem0e  27401  gausslemma2dlem0i  27405  gausslemma2dlem1a  27406  gausslemma2dlem7  27414  gausslemma2d  27415  rpvmasumlem  27528  rpvmasum2  27553  mudivsum  27571  nosepssdm  27727  nosupbnd2lem1  27756  nosupbnd2  27757  noinfbnd2lem1  27771  noetasuplem2  27775  noetasuplem3  27776  noetainflem2  27779  tgldimor  28648  f1otrg  29017  nbusgrvtxm1  29526  wlkp1lem2  29819  pthdlem1  29912  crctcshlem4  29966  crctcshwlkn0  29967  crctcshtrl  29969  wspthsnonn0vne  30063  eupth2eucrct  30365  eupthvdres  30383  eucrctshift  30391  eucrct2eupth1  30392  minvecolem3  31025  acunirnmpt2  32812  acunirnmpt2f  32813  fnpreimac  32822  symgfcoeu  33223  tocycfvres1  33251  tocycfvres2  33252  tocyc01  33259  cycpmconjslem1  33295  cycpmconjslem2  33296  archiabllem1a  33332  znfermltl  33513  qusrn  33556  ressply1invg  33726  ressply1sub  33727  ply1fermltl  33743  dimkerim  33885  fedgmullem2  33888  lvecendof1f1o  33891  evls1fldgencl  33928  algextdeglem5  33979  mdetlap  34090  locfinref  34099  ordtconnlem1  34182  pl1cn  34213  zrhunitpreima  34234  qqhnm  34248  qqhucn  34250  rrexttps  34264  ldgenpisyslem1  34421  ddemeas  34494  1stmbfm  34518  2ndmbfm  34519  omsval  34551  sitgclbn  34601  eulerpartgbij  34630  eulerpartlemgs2  34638  unveldomd  34673  probmeasb  34688  plymulx0  34805  signstres  34833  bnj1098  35043  usgrcyclgt2v  35445  subfacp1lem5  35498  erdsze2lem1  35517  cvmseu  35590  cvmliftlem11  35609  cvmlift3lem8  35640  cvmlift3lem9  35641  trer  36640  meran1  36735  lukshef-ax2  36739  ordcmp  36771  curryset  37395  currysetlem3  37398  bj-snsetex  37412  pibt2  37875  wl-nfeqfb  38003  phpreu  38067  poimirlem1  38084  poimirlem2  38085  poimirlem9  38092  poimirlem18  38101  poimirlem27  38110  poimirlem31  38114  poimirlem32  38115  mblfinlem2  38121  sdclem2  38205  ismtyhmeolem  38267  heiborlem10  38283  notornotel1  38558  mpobi123f  38625  lpssat  39601  lssatle  39603  lssat  39604  cdlemk45  41535  dia2dimlem9  41660  diblsmopel  41759  dochspss  41966  baerlem5blem2  42300  hdmap14lem4a  42459  lcmineqlem2  42611  aks6d1c1p2  42690  aks6d1c1p3  42691  hashscontpowcl  42701  hashscontpow  42703  aks6d1c4  42705  idomnnzpownz  42713  idomnnzgmulnz  42714  aks6d1c6lem3  42753  aks6d1c6lem5  42758  aks6d1c7lem1  42761  aomclem6  43600  kelac1  43604  kelac2  43606  isnumbasgrplem3  43646  proot1mul  43735  ntrclsk3  44610  neicvgel1  44659  ismnushort  44841  choicefi  45741  infleinflem1  45909  supcnvlimsup  46278  stoweidlem11  46549  stoweidlem14  46552  fourierdlem12  46657  fourierdlem51  46695  fourierdlem80  46724  smfresal  47326  simpcntrab  47408  natglobalincr  47417  adh-minim  47559  afv0nbfvbi  47709  iccelpart  48003  fmtnoprmfac2lem1  48139  perfectALTVlem1  48307  bgoldbtbndlem2  48392  cznabel  48846  mgpsumz  48948  uprcl2  49774  lanrcl  50206  ranrcl  50207