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  3705  relopabi  5769  f1ocnvfvrneq  7232  fcof1oinvd  7239  isoselem  7287  isose  7289  fnwelem  8072  tposss  8168  smoiso  8293  nneob  8583  difsnen  8988  php  9132  ordtypelem10  9433  oismo  9446  cantnflt2  9583  oemapso  9592  cantnf  9603  scott0  9799  tskwe  9863  infxpenlem  9924  ac10ct  9945  acndom  9962  dfac12lem2  10056  dfac12r  10058  pwdjudom  10126  ackbij1lem15  10144  ackbij2lem2  10150  ackbij2lem3  10151  ackbij2  10153  fin23lem22  10238  domtriomlem  10353  axdc3lem2  10362  sdomsdomcard  10471  fpwwe2lem8  10550  canthp1lem2  10565  pwfseqlem5  10575  xnn0lem1lt  13185  fzssp1  13510  fzosplitsnm1  13684  fzofzp1  13708  fzostep1  13730  fldiv4lem1div2uz2  13784  fsuppmapnn0fiublem  13941  fsuppmapnn0fiub  13942  bcm1k  14266  pfxccatpfx2  14688  revrev  14718  climuni  15503  isercolllem2  15617  isercoll  15619  serf0  15632  fsumparts  15758  hashiun  15774  isumsup2  15800  climcndslem1  15803  climcndslem2  15804  binomfallfaclem2  15994  2mulprm  16651  oddprm  16770  vdwmc  16938  prdsplusg  17410  prdsvsca  17412  imasdsval2  17469  catcone0  17642  sscpwex  17771  ssc2  17778  pmtrfv  19416  symgtrinv  19436  psgnprfval  19485  odcl2  19529  lsmmod  19639  efgsdmi  19696  gsumzinv  19909  ablfac1b  20036  pgpfac1lem1  20040  pgpfaclem2  20048  ablfaclem2  20052  ablfac  20054  srng0  20820  orngsqr  20832  orngmullt  20837  ofldtos  20839  rmodislmod  20914  znzrh2  21533  znf1o  21539  znhash  21546  znfld  21548  cygznlem3  21557  psgnevpmb  21575  ip2di  21629  mpofrlmd  21765  ascl0  21872  ascl1  21873  mpfsubrg  22098  gsumply1subr  22206  evls1gsumadd  22298  pf1subrg  22322  mpfpf1  22325  pf1mpf  22326  scmatsgrp1  22496  madutpos  22616  iscncl  23243  qtopcmap  23693  hmeores  23745  qtopf1  23790  fbssfi  23811  filssufil  23886  fmfnfmlem3  23930  clssubg  24083  tmsxms  24460  prdsxms  24504  metustfbas  24531  metuel2  24539  restmetu  24544  tngngp2  24626  nrginvrcn  24666  nmhmcn  25096  iscmet3  25269  minveclem3  25405  ovoliunlem2  25479  ismbf3d  25630  i1fd  25657  dvadd  25916  dvmul  25917  dvaddf  25918  dvco  25923  dvcof  25924  dvcnvlem  25952  dgrub  26211  plyremlem  26283  fta1lem  26286  fta1  26287  vieta1lem2  26290  plyexmo  26292  elaa  26295  ulmcau  26375  ulmdvlem3  26382  efabl  26530  relogbf  26772  ppinprm  27133  chtnprm  27135  dchrzrh1  27226  dchr1  27239  dchr1re  27245  dchrptlem1  27246  dchrpt  27249  dchrsum2  27250  dchrhash  27253  gausslemma2dlem0c  27340  gausslemma2dlem0e  27342  gausslemma2dlem0i  27346  gausslemma2dlem1a  27347  gausslemma2dlem7  27355  gausslemma2d  27356  rpvmasumlem  27469  rpvmasum2  27494  mudivsum  27512  nosepssdm  27669  nosupbnd2lem1  27698  nosupbnd2  27699  noinfbnd2lem1  27713  noetasuplem2  27717  noetasuplem3  27718  noetainflem2  27721  tgldimor  28589  f1otrg  28958  nbusgrvtxm1  29467  wlkp1lem2  29761  pthdlem1  29854  crctcshlem4  29908  crctcshwlkn0  29909  crctcshtrl  29911  wspthsnonn0vne  30005  eupth2eucrct  30307  eupthvdres  30325  eucrctshift  30333  eucrct2eupth1  30334  minvecolem3  30967  acunirnmpt2  32753  acunirnmpt2f  32754  fnpreimac  32763  symgfcoeu  33163  tocycfvres1  33191  tocycfvres2  33192  tocyc01  33199  cycpmconjslem1  33235  cycpmconjslem2  33236  archiabllem1a  33272  znfermltl  33446  qusrn  33489  ressply1invg  33649  ressply1sub  33650  ply1fermltl  33666  dimkerim  33792  fedgmullem2  33795  lvecendof1f1o  33798  evls1fldgencl  33835  algextdeglem5  33886  mdetlap  33997  locfinref  34006  ordtconnlem1  34089  pl1cn  34120  zrhunitpreima  34141  qqhnm  34155  qqhucn  34157  rrexttps  34171  ldgenpisyslem1  34328  ddemeas  34401  1stmbfm  34425  2ndmbfm  34426  omsval  34458  sitgclbn  34508  eulerpartgbij  34537  eulerpartlemgs2  34545  unveldomd  34580  probmeasb  34595  plymulx0  34712  signstres  34740  bnj1098  34947  usgrcyclgt2v  35334  subfacp1lem5  35387  erdsze2lem1  35406  cvmseu  35479  cvmliftlem11  35498  cvmlift3lem8  35529  cvmlift3lem9  35530  trer  36519  meran1  36614  lukshef-ax2  36618  ordcmp  36650  curryset  37266  currysetlem3  37269  bj-snsetex  37283  pibt2  37744  wl-nfeqfb  37872  phpreu  37936  poimirlem1  37953  poimirlem2  37954  poimirlem9  37961  poimirlem18  37970  poimirlem27  37979  poimirlem31  37983  poimirlem32  37984  mblfinlem2  37990  sdclem2  38074  ismtyhmeolem  38136  heiborlem10  38152  notornotel1  38427  mpobi123f  38494  lpssat  39470  lssatle  39472  lssat  39473  cdlemk45  41404  dia2dimlem9  41529  diblsmopel  41628  dochspss  41835  baerlem5blem2  42169  hdmap14lem4a  42328  lcmineqlem2  42480  aks6d1c1p2  42559  aks6d1c1p3  42560  hashscontpowcl  42570  hashscontpow  42572  aks6d1c4  42574  idomnnzpownz  42582  idomnnzgmulnz  42583  aks6d1c6lem3  42622  aks6d1c6lem5  42627  aks6d1c7lem1  42630  aomclem6  43502  kelac1  43506  kelac2  43508  isnumbasgrplem3  43548  proot1mul  43637  ntrclsk3  44512  neicvgel1  44561  ismnushort  44743  choicefi  45644  infleinflem1  45814  supcnvlimsup  46183  stoweidlem11  46454  stoweidlem14  46457  fourierdlem12  46562  fourierdlem48  46597  fourierdlem51  46600  fourierdlem80  46629  sssmf  47181  smfresal  47231  simpcntrab  47313  natglobalincr  47320  adh-minim  47446  afv0nbfvbi  47596  iccelpart  47890  fmtnoprmfac2lem1  48026  perfectALTVlem1  48194  bgoldbtbndlem2  48279  cznabel  48733  mgpsumz  48835  uprcl2  49661  lanrcl  50093  ranrcl  50094