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  2738  2reu5  3716  relopabi  5771  f1ocnvfvrneq  7232  fcof1oinvd  7239  isoselem  7287  isose  7289  fnwelem  8073  tposss  8169  smoiso  8294  nneob  8584  difsnen  8987  php  9131  ordtypelem10  9432  oismo  9445  cantnflt2  9582  oemapso  9591  cantnf  9602  scott0  9798  tskwe  9862  infxpenlem  9923  ac10ct  9944  acndom  9961  dfac12lem2  10055  dfac12r  10057  pwdjudom  10125  ackbij1lem15  10143  ackbij2lem2  10149  ackbij2lem3  10150  ackbij2  10152  fin23lem22  10237  domtriomlem  10352  axdc3lem2  10361  sdomsdomcard  10470  fpwwe2lem8  10549  canthp1lem2  10564  pwfseqlem5  10574  xnn0lem1lt  13159  fzssp1  13483  fzosplitsnm1  13656  fzofzp1  13680  fzostep1  13702  fldiv4lem1div2uz2  13756  fsuppmapnn0fiublem  13913  fsuppmapnn0fiub  13914  bcm1k  14238  pfxccatpfx2  14660  revrev  14690  climuni  15475  isercolllem2  15589  isercoll  15591  serf0  15604  fsumparts  15729  hashiun  15745  isumsup2  15769  climcndslem1  15772  climcndslem2  15773  binomfallfaclem2  15963  2mulprm  16620  oddprm  16738  vdwmc  16906  prdsplusg  17378  prdsvsca  17380  imasdsval2  17437  catcone0  17610  sscpwex  17739  ssc2  17746  pmtrfv  19381  symgtrinv  19401  psgnprfval  19450  odcl2  19494  lsmmod  19604  efgsdmi  19661  gsumzinv  19874  ablfac1b  20001  pgpfac1lem1  20005  pgpfaclem2  20013  ablfaclem2  20017  ablfac  20019  srng0  20787  orngsqr  20799  orngmullt  20804  ofldtos  20806  rmodislmod  20881  znzrh2  21500  znf1o  21506  znhash  21513  znfld  21515  cygznlem3  21524  psgnevpmb  21542  ip2di  21596  mpofrlmd  21732  ascl0  21840  ascl1  21841  mpfsubrg  22066  gsumply1subr  22174  evls1gsumadd  22268  pf1subrg  22292  mpfpf1  22295  pf1mpf  22296  scmatsgrp1  22466  madutpos  22586  iscncl  23213  qtopcmap  23663  hmeores  23715  qtopf1  23760  fbssfi  23781  filssufil  23856  fmfnfmlem3  23900  clssubg  24053  tmsxms  24430  prdsxms  24474  metustfbas  24501  metuel2  24509  restmetu  24514  tngngp2  24596  nrginvrcn  24636  nmhmcn  25076  iscmet3  25249  minveclem3  25385  ovoliunlem2  25460  ismbf3d  25611  i1fd  25638  dvadd  25899  dvmul  25900  dvaddf  25901  dvco  25907  dvcof  25908  dvcnvlem  25936  dgrub  26195  plyremlem  26268  fta1lem  26271  fta1  26272  vieta1lem2  26275  plyexmo  26277  elaa  26280  ulmcau  26360  ulmdvlem3  26367  efabl  26515  relogbf  26757  ppinprm  27118  chtnprm  27120  dchrzrh1  27211  dchr1  27224  dchr1re  27230  dchrptlem1  27231  dchrpt  27234  dchrsum2  27235  dchrhash  27238  gausslemma2dlem0c  27325  gausslemma2dlem0e  27327  gausslemma2dlem0i  27331  gausslemma2dlem1a  27332  gausslemma2dlem7  27340  gausslemma2d  27341  rpvmasumlem  27454  rpvmasum2  27479  mudivsum  27497  nosepssdm  27654  nosupbnd2lem1  27683  nosupbnd2  27684  noinfbnd2lem1  27698  noetasuplem2  27702  noetasuplem3  27703  noetainflem2  27706  tgldimor  28574  f1otrg  28943  nbusgrvtxm1  29452  wlkp1lem2  29746  pthdlem1  29839  crctcshlem4  29893  crctcshwlkn0  29894  crctcshtrl  29896  wspthsnonn0vne  29990  eupth2eucrct  30292  eupthvdres  30310  eucrctshift  30318  eucrct2eupth1  30319  minvecolem3  30951  acunirnmpt2  32738  acunirnmpt2f  32739  fnpreimac  32749  symgfcoeu  33164  tocycfvres1  33192  tocycfvres2  33193  tocyc01  33200  cycpmconjslem1  33236  cycpmconjslem2  33237  archiabllem1a  33273  znfermltl  33447  qusrn  33490  ressply1invg  33650  ressply1sub  33651  ply1fermltl  33667  dimkerim  33784  fedgmullem2  33787  lvecendof1f1o  33790  evls1fldgencl  33827  algextdeglem5  33878  mdetlap  33989  locfinref  33998  ordtconnlem1  34081  pl1cn  34112  zrhunitpreima  34133  qqhnm  34147  qqhucn  34149  rrexttps  34163  ldgenpisyslem1  34320  ddemeas  34393  1stmbfm  34417  2ndmbfm  34418  omsval  34450  sitgclbn  34500  eulerpartgbij  34529  eulerpartlemgs2  34537  unveldomd  34572  probmeasb  34587  plymulx0  34704  signstres  34732  bnj1098  34939  usgrcyclgt2v  35325  subfacp1lem5  35378  erdsze2lem1  35397  cvmseu  35470  cvmliftlem11  35489  cvmlift3lem8  35520  cvmlift3lem9  35521  trer  36510  meran1  36605  lukshef-ax2  36609  ordcmp  36641  curryset  37147  currysetlem3  37150  bj-snsetex  37164  pibt2  37618  wl-nfeqfb  37737  phpreu  37801  poimirlem1  37818  poimirlem2  37819  poimirlem9  37826  poimirlem18  37835  poimirlem27  37844  poimirlem31  37848  poimirlem32  37849  mblfinlem2  37855  sdclem2  37939  ismtyhmeolem  38001  heiborlem10  38017  notornotel1  38292  mpobi123f  38359  lpssat  39269  lssatle  39271  lssat  39272  cdlemk45  41203  dia2dimlem9  41328  diblsmopel  41427  dochspss  41634  baerlem5blem2  41968  hdmap14lem4a  42127  lcmineqlem2  42280  aks6d1c1p2  42359  aks6d1c1p3  42360  hashscontpowcl  42370  hashscontpow  42372  aks6d1c4  42374  idomnnzpownz  42382  idomnnzgmulnz  42383  aks6d1c6lem3  42422  aks6d1c6lem5  42427  aks6d1c7lem1  42430  aomclem6  43297  kelac1  43301  kelac2  43303  isnumbasgrplem3  43343  proot1mul  43432  ntrclsk3  44307  neicvgel1  44356  ismnushort  44538  choicefi  45440  infleinflem1  45610  supcnvlimsup  45980  stoweidlem11  46251  stoweidlem14  46254  fourierdlem12  46359  fourierdlem48  46394  fourierdlem51  46397  fourierdlem80  46426  sssmf  46978  smfresal  47028  simpcntrab  47110  natglobalincr  47117  adh-minim  47243  afv0nbfvbi  47393  iccelpart  47675  fmtnoprmfac2lem1  47808  perfectALTVlem1  47963  bgoldbtbndlem2  48048  cznabel  48502  mgpsumz  48604  uprcl2  49430  lanrcl  49862  ranrcl  49863