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  2059  eqeq1d  2739  2reu5  3718  relopabi  5779  f1ocnvfvrneq  7242  fcof1oinvd  7249  isoselem  7297  isose  7299  fnwelem  8083  tposss  8179  smoiso  8304  nneob  8594  difsnen  8999  php  9143  ordtypelem10  9444  oismo  9457  cantnflt2  9594  oemapso  9603  cantnf  9614  scott0  9810  tskwe  9874  infxpenlem  9935  ac10ct  9956  acndom  9973  dfac12lem2  10067  dfac12r  10069  pwdjudom  10137  ackbij1lem15  10155  ackbij2lem2  10161  ackbij2lem3  10162  ackbij2  10164  fin23lem22  10249  domtriomlem  10364  axdc3lem2  10373  sdomsdomcard  10482  fpwwe2lem8  10561  canthp1lem2  10576  pwfseqlem5  10586  xnn0lem1lt  13171  fzssp1  13495  fzosplitsnm1  13668  fzofzp1  13692  fzostep1  13714  fldiv4lem1div2uz2  13768  fsuppmapnn0fiublem  13925  fsuppmapnn0fiub  13926  bcm1k  14250  pfxccatpfx2  14672  revrev  14702  climuni  15487  isercolllem2  15601  isercoll  15603  serf0  15616  fsumparts  15741  hashiun  15757  isumsup2  15781  climcndslem1  15784  climcndslem2  15785  binomfallfaclem2  15975  2mulprm  16632  oddprm  16750  vdwmc  16918  prdsplusg  17390  prdsvsca  17392  imasdsval2  17449  catcone0  17622  sscpwex  17751  ssc2  17758  pmtrfv  19393  symgtrinv  19413  psgnprfval  19462  odcl2  19506  lsmmod  19616  efgsdmi  19673  gsumzinv  19886  ablfac1b  20013  pgpfac1lem1  20017  pgpfaclem2  20025  ablfaclem2  20029  ablfac  20031  srng0  20799  orngsqr  20811  orngmullt  20816  ofldtos  20818  rmodislmod  20893  znzrh2  21512  znf1o  21518  znhash  21525  znfld  21527  cygznlem3  21536  psgnevpmb  21554  ip2di  21608  mpofrlmd  21744  ascl0  21852  ascl1  21853  mpfsubrg  22078  gsumply1subr  22186  evls1gsumadd  22280  pf1subrg  22304  mpfpf1  22307  pf1mpf  22308  scmatsgrp1  22478  madutpos  22598  iscncl  23225  qtopcmap  23675  hmeores  23727  qtopf1  23772  fbssfi  23793  filssufil  23868  fmfnfmlem3  23912  clssubg  24065  tmsxms  24442  prdsxms  24486  metustfbas  24513  metuel2  24521  restmetu  24526  tngngp2  24608  nrginvrcn  24648  nmhmcn  25088  iscmet3  25261  minveclem3  25397  ovoliunlem2  25472  ismbf3d  25623  i1fd  25650  dvadd  25911  dvmul  25912  dvaddf  25913  dvco  25919  dvcof  25920  dvcnvlem  25948  dgrub  26207  plyremlem  26280  fta1lem  26283  fta1  26284  vieta1lem2  26287  plyexmo  26289  elaa  26292  ulmcau  26372  ulmdvlem3  26379  efabl  26527  relogbf  26769  ppinprm  27130  chtnprm  27132  dchrzrh1  27223  dchr1  27236  dchr1re  27242  dchrptlem1  27243  dchrpt  27246  dchrsum2  27247  dchrhash  27250  gausslemma2dlem0c  27337  gausslemma2dlem0e  27339  gausslemma2dlem0i  27343  gausslemma2dlem1a  27344  gausslemma2dlem7  27352  gausslemma2d  27353  rpvmasumlem  27466  rpvmasum2  27491  mudivsum  27509  nosepssdm  27666  nosupbnd2lem1  27695  nosupbnd2  27696  noinfbnd2lem1  27710  noetasuplem2  27714  noetasuplem3  27715  noetainflem2  27718  tgldimor  28586  f1otrg  28955  nbusgrvtxm1  29464  wlkp1lem2  29758  pthdlem1  29851  crctcshlem4  29905  crctcshwlkn0  29906  crctcshtrl  29908  wspthsnonn0vne  30002  eupth2eucrct  30304  eupthvdres  30322  eucrctshift  30330  eucrct2eupth1  30331  minvecolem3  30963  acunirnmpt2  32749  acunirnmpt2f  32750  fnpreimac  32759  symgfcoeu  33175  tocycfvres1  33203  tocycfvres2  33204  tocyc01  33211  cycpmconjslem1  33247  cycpmconjslem2  33248  archiabllem1a  33284  znfermltl  33458  qusrn  33501  ressply1invg  33661  ressply1sub  33662  ply1fermltl  33678  dimkerim  33804  fedgmullem2  33807  lvecendof1f1o  33810  evls1fldgencl  33847  algextdeglem5  33898  mdetlap  34009  locfinref  34018  ordtconnlem1  34101  pl1cn  34132  zrhunitpreima  34153  qqhnm  34167  qqhucn  34169  rrexttps  34183  ldgenpisyslem1  34340  ddemeas  34413  1stmbfm  34437  2ndmbfm  34438  omsval  34470  sitgclbn  34520  eulerpartgbij  34549  eulerpartlemgs2  34557  unveldomd  34592  probmeasb  34607  plymulx0  34724  signstres  34752  bnj1098  34959  usgrcyclgt2v  35344  subfacp1lem5  35397  erdsze2lem1  35416  cvmseu  35489  cvmliftlem11  35508  cvmlift3lem8  35539  cvmlift3lem9  35540  trer  36529  meran1  36624  lukshef-ax2  36628  ordcmp  36660  curryset  37191  currysetlem3  37194  bj-snsetex  37208  pibt2  37669  wl-nfeqfb  37788  phpreu  37852  poimirlem1  37869  poimirlem2  37870  poimirlem9  37877  poimirlem18  37886  poimirlem27  37895  poimirlem31  37899  poimirlem32  37900  mblfinlem2  37906  sdclem2  37990  ismtyhmeolem  38052  heiborlem10  38068  notornotel1  38343  mpobi123f  38410  lpssat  39386  lssatle  39388  lssat  39389  cdlemk45  41320  dia2dimlem9  41445  diblsmopel  41544  dochspss  41751  baerlem5blem2  42085  hdmap14lem4a  42244  lcmineqlem2  42397  aks6d1c1p2  42476  aks6d1c1p3  42477  hashscontpowcl  42487  hashscontpow  42489  aks6d1c4  42491  idomnnzpownz  42499  idomnnzgmulnz  42500  aks6d1c6lem3  42539  aks6d1c6lem5  42544  aks6d1c7lem1  42547  aomclem6  43413  kelac1  43417  kelac2  43419  isnumbasgrplem3  43459  proot1mul  43548  ntrclsk3  44423  neicvgel1  44472  ismnushort  44654  choicefi  45555  infleinflem1  45725  supcnvlimsup  46095  stoweidlem11  46366  stoweidlem14  46369  fourierdlem12  46474  fourierdlem48  46509  fourierdlem51  46512  fourierdlem80  46541  sssmf  47093  smfresal  47143  simpcntrab  47225  natglobalincr  47232  adh-minim  47358  afv0nbfvbi  47508  iccelpart  47790  fmtnoprmfac2lem1  47923  perfectALTVlem1  48078  bgoldbtbndlem2  48163  cznabel  48617  mgpsumz  48719  uprcl2  49545  lanrcl  49977  ranrcl  49978