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  2056  eqeq1d  2731  2reu5  3729  relopabi  5785  f1ocnvfvrneq  7261  fcof1oinvd  7268  isoselem  7316  isose  7318  fnwelem  8110  tposss  8206  smoiso  8331  nneob  8620  difsnen  9023  php  9171  ordtypelem10  9480  oismo  9493  cantnflt2  9626  oemapso  9635  cantnf  9646  scott0  9839  tskwe  9903  infxpenlem  9966  ac10ct  9987  acndom  10004  dfac12lem2  10098  dfac12r  10100  pwdjudom  10168  ackbij1lem15  10186  ackbij2lem2  10192  ackbij2lem3  10193  ackbij2  10195  fin23lem22  10280  domtriomlem  10395  axdc3lem2  10404  sdomsdomcard  10513  fpwwe2lem8  10591  canthp1lem2  10606  pwfseqlem5  10616  xnn0lem1lt  13204  fzssp1  13528  fzosplitsnm1  13701  fzofzp1  13725  fzostep1  13744  fldiv4lem1div2uz2  13798  fsuppmapnn0fiublem  13955  fsuppmapnn0fiub  13956  bcm1k  14280  pfxccatpfx2  14702  revrev  14732  climuni  15518  isercolllem2  15632  isercoll  15634  serf0  15647  fsumparts  15772  hashiun  15788  isumsup2  15812  climcndslem1  15815  climcndslem2  15816  binomfallfaclem2  16006  2mulprm  16663  oddprm  16781  vdwmc  16949  prdsplusg  17421  prdsvsca  17423  imasdsval2  17479  catcone0  17648  sscpwex  17777  ssc2  17784  pmtrfv  19382  symgtrinv  19402  psgnprfval  19451  odcl2  19495  lsmmod  19605  efgsdmi  19662  gsumzinv  19875  ablfac1b  20002  pgpfac1lem1  20006  pgpfaclem2  20014  ablfaclem2  20018  ablfac  20020  srng0  20763  rmodislmod  20836  znzrh2  21455  znf1o  21461  znhash  21468  znfld  21470  cygznlem3  21479  psgnevpmb  21496  ip2di  21550  mpofrlmd  21686  ascl0  21793  ascl1  21794  mpfsubrg  22010  gsumply1subr  22118  evls1gsumadd  22211  pf1subrg  22235  mpfpf1  22238  pf1mpf  22239  scmatsgrp1  22409  madutpos  22529  iscncl  23156  qtopcmap  23606  hmeores  23658  qtopf1  23703  fbssfi  23724  filssufil  23799  fmfnfmlem3  23843  clssubg  23996  tmsxms  24374  prdsxms  24418  metustfbas  24445  metuel2  24453  restmetu  24458  tngngp2  24540  nrginvrcn  24580  nmhmcn  25020  iscmet3  25193  minveclem3  25329  ovoliunlem2  25404  ismbf3d  25555  i1fd  25582  dvadd  25843  dvmul  25844  dvaddf  25845  dvco  25851  dvcof  25852  dvcnvlem  25880  dgrub  26139  plyremlem  26212  fta1lem  26215  fta1  26216  vieta1lem2  26219  plyexmo  26221  elaa  26224  ulmcau  26304  ulmdvlem3  26311  efabl  26459  relogbf  26701  ppinprm  27062  chtnprm  27064  dchrzrh1  27155  dchr1  27168  dchr1re  27174  dchrptlem1  27175  dchrpt  27178  dchrsum2  27179  dchrhash  27182  gausslemma2dlem0c  27269  gausslemma2dlem0e  27271  gausslemma2dlem0i  27275  gausslemma2dlem1a  27276  gausslemma2dlem7  27284  gausslemma2d  27285  rpvmasumlem  27398  rpvmasum2  27423  mudivsum  27441  nosepssdm  27598  nosupbnd2lem1  27627  nosupbnd2  27628  noinfbnd2lem1  27642  noetasuplem2  27646  noetasuplem3  27647  noetainflem2  27650  tgldimor  28429  f1otrg  28798  nbusgrvtxm1  29306  wlkp1lem2  29602  pthdlem1  29696  crctcshlem4  29750  crctcshwlkn0  29751  crctcshtrl  29753  wspthsnonn0vne  29847  eupth2eucrct  30146  eupthvdres  30164  eucrctshift  30172  eucrct2eupth1  30173  minvecolem3  30805  acunirnmpt2  32584  acunirnmpt2f  32585  fnpreimac  32595  symgfcoeu  33039  tocycfvres1  33067  tocycfvres2  33068  tocyc01  33075  cycpmconjslem1  33111  cycpmconjslem2  33112  archiabllem1a  33145  orngsqr  33282  orngmullt  33287  ofldtos  33289  znfermltl  33337  qusrn  33380  ressply1invg  33538  ressply1sub  33539  ply1fermltl  33553  dimkerim  33623  fedgmullem2  33626  lvecendof1f1o  33629  evls1fldgencl  33665  algextdeglem5  33711  mdetlap  33822  locfinref  33831  ordtconnlem1  33914  pl1cn  33945  zrhunitpreima  33966  qqhnm  33980  qqhucn  33982  rrexttps  33996  ldgenpisyslem1  34153  ddemeas  34226  1stmbfm  34251  2ndmbfm  34252  omsval  34284  sitgclbn  34334  eulerpartgbij  34363  eulerpartlemgs2  34371  unveldomd  34406  probmeasb  34421  plymulx0  34538  signstres  34566  bnj1098  34773  usgrcyclgt2v  35118  subfacp1lem5  35171  erdsze2lem1  35190  cvmseu  35263  cvmliftlem11  35282  cvmlift3lem8  35313  cvmlift3lem9  35314  trer  36304  meran1  36399  lukshef-ax2  36403  ordcmp  36435  curryset  36934  currysetlem3  36937  bj-snsetex  36951  pibt2  37405  wl-nfeqfb  37524  phpreu  37598  poimirlem1  37615  poimirlem2  37616  poimirlem9  37623  poimirlem18  37632  poimirlem27  37641  poimirlem31  37645  poimirlem32  37646  mblfinlem2  37652  sdclem2  37736  ismtyhmeolem  37798  heiborlem10  37814  notornotel1  38089  mpobi123f  38156  lpssat  39006  lssatle  39008  lssat  39009  cdlemk45  40941  dia2dimlem9  41066  diblsmopel  41165  dochspss  41372  baerlem5blem2  41706  hdmap14lem4a  41865  lcmineqlem2  42018  aks6d1c1p2  42097  aks6d1c1p3  42098  hashscontpowcl  42108  hashscontpow  42110  aks6d1c4  42112  idomnnzpownz  42120  idomnnzgmulnz  42121  aks6d1c6lem3  42160  aks6d1c6lem5  42165  aks6d1c7lem1  42168  aomclem6  43048  kelac1  43052  kelac2  43054  isnumbasgrplem3  43094  proot1mul  43183  ntrclsk3  44059  neicvgel1  44108  ismnushort  44290  choicefi  45194  infleinflem1  45366  supcnvlimsup  45738  stoweidlem11  46009  stoweidlem14  46012  fourierdlem12  46117  fourierdlem48  46152  fourierdlem51  46155  fourierdlem80  46184  sssmf  46736  smfresal  46786  simpcntrab  46868  natglobalincr  46875  adh-minim  47002  afv0nbfvbi  47152  iccelpart  47434  fmtnoprmfac2lem1  47567  perfectALTVlem1  47722  bgoldbtbndlem2  47807  cznabel  48248  mgpsumz  48350  uprcl2  49178  lanrcl  49610  ranrcl  49611