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  2053  eqeq1d  2737  2reu5  3767  relopabi  5835  f1ocnvfvrneq  7306  fcof1oinvd  7313  isoselem  7361  isose  7363  fnwelem  8155  tposss  8251  wfrlem5OLD  8352  smoiso  8401  nneob  8693  difsnen  9092  php  9245  ordtypelem10  9565  oismo  9578  cantnflt2  9711  oemapso  9720  cantnf  9731  scott0  9924  tskwe  9988  infxpenlem  10051  ac10ct  10072  acndom  10089  dfac12lem2  10183  dfac12r  10185  pwdjudom  10253  ackbij1lem15  10271  ackbij2lem2  10277  ackbij2lem3  10278  ackbij2  10280  fin23lem22  10365  domtriomlem  10480  axdc3lem2  10489  sdomsdomcard  10598  fpwwe2lem8  10676  canthp1lem2  10691  pwfseqlem5  10701  xnn0lem1lt  13283  fzssp1  13604  fzosplitsnm1  13776  fzofzp1  13800  fzostep1  13819  fldiv4lem1div2uz2  13873  fsuppmapnn0fiublem  14028  fsuppmapnn0fiub  14029  bcm1k  14351  pfxccatpfx2  14772  revrev  14802  climuni  15585  isercolllem2  15699  isercoll  15701  serf0  15714  fsumparts  15839  hashiun  15855  isumsup2  15879  climcndslem1  15882  climcndslem2  15883  binomfallfaclem2  16073  2mulprm  16727  oddprm  16844  vdwmc  17012  prdsplusg  17505  prdsvsca  17507  imasdsval2  17563  catcone0  17732  sscpwex  17863  ssc2  17870  pmtrfv  19485  symgtrinv  19505  psgnprfval  19554  odcl2  19598  lsmmod  19708  efgsdmi  19765  gsumzinv  19978  ablfac1b  20105  pgpfac1lem1  20109  pgpfaclem2  20117  ablfaclem2  20121  ablfac  20123  srng0  20872  rmodislmod  20945  znzrh2  21582  znf1o  21588  znhash  21595  znfld  21597  cygznlem3  21606  psgnevpmb  21623  ip2di  21677  mpofrlmd  21815  ascl0  21922  ascl1  21923  mpfsubrg  22145  gsumply1subr  22251  evls1gsumadd  22344  pf1subrg  22368  mpfpf1  22371  pf1mpf  22372  scmatsgrp1  22544  madutpos  22664  iscncl  23293  qtopcmap  23743  hmeores  23795  qtopf1  23840  fbssfi  23861  filssufil  23936  fmfnfmlem3  23980  clssubg  24133  tmsxms  24515  prdsxms  24559  metustfbas  24586  metuel2  24594  restmetu  24599  tngngp2  24689  nrginvrcn  24729  nmhmcn  25167  iscmet3  25341  minveclem3  25477  ovoliunlem2  25552  ismbf3d  25703  i1fd  25730  dvadd  25992  dvmul  25993  dvaddf  25994  dvco  26000  dvcof  26001  dvcnvlem  26029  dgrub  26288  plyremlem  26361  fta1lem  26364  fta1  26365  vieta1lem2  26368  plyexmo  26370  elaa  26373  ulmcau  26453  ulmdvlem3  26460  efabl  26607  relogbf  26849  ppinprm  27210  chtnprm  27212  dchrzrh1  27303  dchr1  27316  dchr1re  27322  dchrptlem1  27323  dchrpt  27326  dchrsum2  27327  dchrhash  27330  gausslemma2dlem0c  27417  gausslemma2dlem0e  27419  gausslemma2dlem0i  27423  gausslemma2dlem1a  27424  gausslemma2dlem7  27432  gausslemma2d  27433  rpvmasumlem  27546  rpvmasum2  27571  mudivsum  27589  nosepssdm  27746  nosupbnd2lem1  27775  nosupbnd2  27776  noinfbnd2lem1  27790  noetasuplem2  27794  noetasuplem3  27795  noetainflem2  27798  tgldimor  28525  f1otrg  28894  nbusgrvtxm1  29411  wlkp1lem2  29707  pthdlem1  29799  crctcshlem4  29850  crctcshwlkn0  29851  crctcshtrl  29853  wspthsnonn0vne  29947  eupth2eucrct  30246  eupthvdres  30264  eucrctshift  30272  eucrct2eupth1  30273  minvecolem3  30905  acunirnmpt2  32677  acunirnmpt2f  32678  fnpreimac  32688  symgfcoeu  33085  tocycfvres1  33113  tocycfvres2  33114  tocyc01  33121  cycpmconjslem1  33157  cycpmconjslem2  33158  archiabllem1a  33181  orngsqr  33314  orngmullt  33319  ofldtos  33321  znfermltl  33374  qusrn  33417  ressply1invg  33574  ressply1sub  33575  ply1fermltl  33589  dimkerim  33655  fedgmullem2  33658  lvecendof1f1o  33661  evls1fldgencl  33695  algextdeglem5  33727  mdetlap  33793  locfinref  33802  ordtconnlem1  33885  pl1cn  33916  zrhunitpreima  33939  qqhnm  33953  qqhucn  33955  rrexttps  33969  ldgenpisyslem1  34144  ddemeas  34217  1stmbfm  34242  2ndmbfm  34243  omsval  34275  sitgclbn  34325  eulerpartgbij  34354  eulerpartlemgs2  34362  unveldomd  34397  probmeasb  34412  plymulx0  34541  signstres  34569  bnj1098  34776  usgrcyclgt2v  35116  subfacp1lem5  35169  erdsze2lem1  35188  cvmseu  35261  cvmliftlem11  35280  cvmlift3lem8  35311  cvmlift3lem9  35312  trer  36299  meran1  36394  lukshef-ax2  36398  ordcmp  36430  curryset  36929  currysetlem3  36932  bj-snsetex  36946  pibt2  37400  wl-nfeqfb  37517  phpreu  37591  poimirlem1  37608  poimirlem2  37609  poimirlem9  37616  poimirlem18  37625  poimirlem27  37634  poimirlem31  37638  poimirlem32  37639  mblfinlem2  37645  sdclem2  37729  ismtyhmeolem  37791  heiborlem10  37807  notornotel1  38082  mpobi123f  38149  lpssat  38995  lssatle  38997  lssat  38998  cdlemk45  40930  dia2dimlem9  41055  diblsmopel  41154  dochspss  41361  baerlem5blem2  41695  hdmap14lem4a  41854  lcmineqlem2  42012  aks6d1c1p2  42091  aks6d1c1p3  42092  hashscontpowcl  42102  hashscontpow  42104  aks6d1c4  42106  idomnnzpownz  42114  idomnnzgmulnz  42115  aks6d1c6lem3  42154  aks6d1c6lem5  42159  aks6d1c7lem1  42162  aomclem6  43048  kelac1  43052  kelac2  43054  isnumbasgrplem3  43094  proot1mul  43183  ntrclsk3  44060  neicvgel1  44109  ismnushort  44297  choicefi  45143  infleinflem1  45320  supcnvlimsup  45696  stoweidlem11  45967  stoweidlem14  45970  fourierdlem12  46075  fourierdlem48  46110  fourierdlem51  46113  fourierdlem80  46142  sssmf  46694  smfresal  46744  simpcntrab  46826  natglobalincr  46831  adh-minim  46951  afv0nbfvbi  47101  iccelpart  47358  fmtnoprmfac2lem1  47491  perfectALTVlem1  47646  bgoldbtbndlem2  47731  cznabel  48104  mgpsumz  48207