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  2064  eqeq1d  2742  2reu5  3706  relopabi  5772  f1ocnvfvrneq  7237  fcof1oinvd  7244  isoselem  7292  isose  7294  fnwelem  8078  tposss  8174  smoiso  8299  nneob  8589  difsnen  8994  php  9138  ordtypelem10  9439  oismo  9452  cantnflt2  9592  oemapso  9601  cantnf  9612  scott0  9808  tskwe  9872  infxpenlem  9933  ac10ct  9954  acndom  9971  dfac12lem2  10065  dfac12r  10067  pwdjudom  10135  ackbij1lem15  10153  ackbij2lem2  10159  ackbij2lem3  10160  ackbij2  10162  fin23lem22  10247  domtriomlem  10362  axdc3lem2  10371  sdomsdomcard  10480  fpwwe2lem8  10559  canthp1lem2  10574  pwfseqlem5  10584  xnn0lem1lt  13194  fzssp1  13519  fzosplitsnm1  13693  fzofzp1  13717  fzostep1  13739  fldiv4lem1div2uz2  13793  fsuppmapnn0fiublem  13950  fsuppmapnn0fiub  13951  bcm1k  14275  pfxccatpfx2  14697  revrev  14727  climuni  15512  isercolllem2  15626  isercoll  15628  serf0  15641  fsumparts  15767  hashiun  15783  isumsup2  15809  climcndslem1  15812  climcndslem2  15813  binomfallfaclem2  16003  2mulprm  16660  oddprm  16779  vdwmc  16947  prdsplusg  17419  prdsvsca  17421  imasdsval2  17478  catcone0  17651  sscpwex  17780  ssc2  17787  pmtrfv  19425  symgtrinv  19445  psgnprfval  19494  odcl2  19538  lsmmod  19648  efgsdmi  19705  gsumzinv  19918  ablfac1b  20045  pgpfac1lem1  20049  pgpfaclem2  20057  ablfaclem2  20061  ablfac  20063  srng0  20833  orngsqr  20845  orngmullt  20850  ofldtos  20852  rmodislmod  20927  znzrh2  21527  znf1o  21533  znhash  21540  znfld  21542  cygznlem3  21551  psgnevpmb  21569  ip2di  21623  mpofrlmd  21759  ascl0  21866  ascl1  21867  mpfsubrg  22094  gsumply1subr  22225  evls1gsumadd  22317  pf1subrg  22341  mpfpf1  22344  pf1mpf  22345  scmatsgrp1  22512  madutpos  22632  iscncl  23259  qtopcmap  23709  hmeores  23761  qtopf1  23806  fbssfi  23827  filssufil  23902  fmfnfmlem3  23946  clssubg  24099  tmsxms  24476  prdsxms  24520  metustfbas  24547  metuel2  24555  restmetu  24560  tngngp2  24642  nrginvrcn  24682  nmhmcn  25112  iscmet3  25285  minveclem3  25421  ovoliunlem2  25495  ismbf3d  25646  i1fd  25673  dvadd  25932  dvmul  25933  dvaddf  25934  dvco  25939  dvcof  25940  dvcnvlem  25968  dgrub  26224  plyremlem  26295  fta1lem  26298  fta1  26299  vieta1lem2  26302  plyexmo  26304  elaa  26307  ulmcau  26385  ulmdvlem3  26392  efabl  26539  relogbf  26780  ppinprm  27140  chtnprm  27142  dchrzrh1  27232  dchr1  27245  dchr1re  27251  dchrptlem1  27252  dchrpt  27255  dchrsum2  27256  dchrhash  27259  gausslemma2dlem0c  27346  gausslemma2dlem0e  27348  gausslemma2dlem0i  27352  gausslemma2dlem1a  27353  gausslemma2dlem7  27361  gausslemma2d  27362  rpvmasumlem  27475  rpvmasum2  27500  mudivsum  27518  nosepssdm  27675  nosupbnd2lem1  27704  nosupbnd2  27705  noinfbnd2lem1  27719  noetasuplem2  27723  noetasuplem3  27724  noetainflem2  27727  tgldimor  28595  f1otrg  28964  nbusgrvtxm1  29473  wlkp1lem2  29766  pthdlem1  29859  crctcshlem4  29913  crctcshwlkn0  29914  crctcshtrl  29916  wspthsnonn0vne  30010  eupth2eucrct  30312  eupthvdres  30330  eucrctshift  30338  eucrct2eupth1  30339  minvecolem3  30972  acunirnmpt2  32759  acunirnmpt2f  32760  fnpreimac  32769  symgfcoeu  33170  tocycfvres1  33198  tocycfvres2  33199  tocyc01  33206  cycpmconjslem1  33242  cycpmconjslem2  33243  archiabllem1a  33279  znfermltl  33456  qusrn  33499  ressply1invg  33659  ressply1sub  33660  ply1fermltl  33676  dimkerim  33818  fedgmullem2  33821  lvecendof1f1o  33824  evls1fldgencl  33861  algextdeglem5  33912  mdetlap  34023  locfinref  34032  ordtconnlem1  34115  pl1cn  34146  zrhunitpreima  34167  qqhnm  34181  qqhucn  34183  rrexttps  34197  ldgenpisyslem1  34354  ddemeas  34427  1stmbfm  34451  2ndmbfm  34452  omsval  34484  sitgclbn  34534  eulerpartgbij  34563  eulerpartlemgs2  34571  unveldomd  34606  probmeasb  34621  plymulx0  34738  signstres  34766  bnj1098  34973  usgrcyclgt2v  35366  subfacp1lem5  35419  erdsze2lem1  35438  cvmseu  35511  cvmliftlem11  35530  cvmlift3lem8  35561  cvmlift3lem9  35562  trer  36551  meran1  36646  lukshef-ax2  36650  ordcmp  36682  curryset  37306  currysetlem3  37309  bj-snsetex  37323  pibt2  37786  wl-nfeqfb  37914  phpreu  37978  poimirlem1  37995  poimirlem2  37996  poimirlem9  38003  poimirlem18  38012  poimirlem27  38021  poimirlem31  38025  poimirlem32  38026  mblfinlem2  38032  sdclem2  38116  ismtyhmeolem  38178  heiborlem10  38194  notornotel1  38469  mpobi123f  38536  lpssat  39512  lssatle  39514  lssat  39515  cdlemk45  41446  dia2dimlem9  41571  diblsmopel  41670  dochspss  41877  baerlem5blem2  42211  hdmap14lem4a  42370  lcmineqlem2  42522  aks6d1c1p2  42601  aks6d1c1p3  42602  hashscontpowcl  42612  hashscontpow  42614  aks6d1c4  42616  idomnnzpownz  42624  idomnnzgmulnz  42625  aks6d1c6lem3  42664  aks6d1c6lem5  42669  aks6d1c7lem1  42672  aomclem6  43511  kelac1  43515  kelac2  43517  isnumbasgrplem3  43557  proot1mul  43646  ntrclsk3  44521  neicvgel1  44570  ismnushort  44752  choicefi  45653  infleinflem1  45821  supcnvlimsup  46190  stoweidlem11  46461  stoweidlem14  46464  fourierdlem12  46569  fourierdlem48  46604  fourierdlem51  46607  fourierdlem80  46636  sssmf  47188  smfresal  47238  simpcntrab  47320  natglobalincr  47329  adh-minim  47471  afv0nbfvbi  47621  iccelpart  47915  fmtnoprmfac2lem1  48051  perfectALTVlem1  48219  bgoldbtbndlem2  48304  cznabel  48758  mgpsumz  48860  uprcl2  49686  lanrcl  50118  ranrcl  50119