Theorem 4syl 20

Description: Inference chaining three syllogisms syl 18. (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 19	. 2 ⊢ (𝜑 → 𝜃)
5		4syl.4	. 2 ⊢ (𝜃 → 𝜏)
6	4, 5	syl 18	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  2080  eqeq1d  2767  2reu5  3724  relopabi  5800  f1ocnvfvrneq  7274  fcof1oinvd  7281  isoselem  7329  isose  7331  fnwelem  8115  tposss  8211  smoiso  8337  nneob  8630  difsnen  9035  php  9179  ordtypelem10  9477  oismo  9490  cantnflt2  9630  oemapso  9639  cantnf  9650  scott0  9848  tskwe  9924  infxpenlem  9985  ac10ct  10006  acndom  10023  dfac12lem2  10116  dfac12r  10118  pwdjudom  10186  ackbij1lem15  10204  ackbij2lem2  10210  ackbij2lem3  10211  ackbij2  10213  fin23lem22  10299  domtriomlem  10414  axdc3lem2  10423  sdomsdomcard  10532  fpwwe2lem8  10611  canthp1lem2  10626  pwfseqlem5  10636  xnn0lem1lt  13261  fzssp1  13586  fzosplitsnm1  13760  fzofzp1  13784  fzostep1  13806  fldiv4lem1div2uz2  13860  fsuppmapnn0fiublem  14017  fsuppmapnn0fiub  14018  bcm1k  14342  pfxccatpfx2  14764  revrev  14794  climuni  15593  isercolllem2  15707  isercoll  15709  serf0  15722  fsumparts  15848  hashiun  15864  isumsup2  15890  climcndslem1  15893  climcndslem2  15894  binomfallfaclem2  16084  2mulprm  16741  oddprm  16860  vdwmc  17028  prdsplusg  17501  prdsvsca  17503  imasdsval2  17560  catcone0  17733  sscpwex  17862  ssc2  17869  pmtrfv  19513  symgtrinv  19533  psgnprfval  19582  odcl2  19626  lsmmod  19736  efgsdmi  19793  gsumzinv  20006  ablfac1b  20133  pgpfac1lem1  20137  pgpfaclem2  20145  ablfaclem2  20149  ablfac  20151  srng0  20926  orngsqr  20938  orngmullt  20943  ofldtos  20945  rmodislmod  21020  znzrh2  21655  znf1o  21661  znhash  21668  znfld  21670  cygznlem3  21679  psgnevpmb  21697  ip2di  21751  mpofrlmd  21887  ascl0  21994  ascl1  21995  mpfsubrg  22222  gsumply1subr  22353  evls1gsumadd  22445  pf1subrg  22469  mpfpf1  22472  pf1mpf  22473  scmatsgrp1  22640  madutpos  22760  iscncl  23387  qtopcmap  23837  hmeores  23889  qtopf1  23934  fbssfi  23955  filssufil  24030  fmfnfmlem3  24074  clssubg  24227  tmsxms  24604  prdsxms  24648  metustfbas  24675  metuel2  24683  restmetu  24688  tngngp2  24770  nrginvrcn  24810  nmhmcn  25240  iscmet3  25413  minveclem3  25549  ovoliunlem2  25623  ismbf3d  25774  i1fd  25801  dvadd  26060  dvmul  26061  dvaddf  26062  dvco  26067  dvcof  26068  dvcnvlem  26096  dgrub  26352  plyn0mulidp  26403  plyremlem  26426  fta1lem  26429  fta1  26430  vieta1lem2  26433  plyexmo  26435  elaa  26438  ulmcau  26516  ulmdvlem3  26523  efabl  26673  relogbf  26914  ppinprm  27274  chtnprm  27276  dchrzrh1  27366  dchr1  27379  dchr1re  27385  dchrptlem1  27386  dchrpt  27389  dchrsum2  27390  dchrhash  27393  gausslemma2dlem0c  27480  gausslemma2dlem0e  27482  gausslemma2dlem0i  27486  gausslemma2dlem1a  27487  gausslemma2dlem7  27495  gausslemma2d  27496  rpvmasumlem  27609  rpvmasum2  27634  mudivsum  27652  nosepssdm  27808  nosupbnd2lem1  27837  nosupbnd2  27838  noinfbnd2lem1  27852  noetasuplem2  27856  noetasuplem3  27857  noetainflem2  27860  tgldimor  28729  f1otrg  29129  nbusgrvtxm1  29638  wlkp1lem2  29931  pthdlem1  30024  crctcshlem4  30078  crctcshwlkn0  30079  crctcshtrl  30081  wspthsnonn0vne  30175  eupth2eucrct  30477  eupthvdres  30495  eucrctshift  30503  eucrct2eupth1  30504  minvecolem3  31137  acunirnmpt2  32917  acunirnmpt2f  32918  fnpreimac  32927  symgfcoeu  33315  tocycfvres1  33343  tocycfvres2  33344  tocyc01  33351  cycpmconjslem1  33387  cycpmconjslem2  33388  archiabllem1a  33424  znfermltl  33596  qusrn  33634  ressply1invg  33776  ressply1sub  33777  ply1fermltl  33793  dimkerim  33934  fedgmullem2  33937  lvecendof1f1o  33940  evls1fldgencl  33977  algextdeglem5  34028  mdetlap  34139  locfinref  34148  ordtconnlem1  34231  pl1cn  34262  zrhunitpreima  34283  qqhnm  34297  qqhucn  34299  rrexttps  34313  ldgenpisyslem1  34470  ddemeas  34543  1stmbfm  34567  2ndmbfm  34568  omsval  34600  sitgclbn  34650  eulerpartgbij  34679  eulerpartlemgs2  34687  unveldomd  34722  probmeasb  34737  signstres  34879  bnj1098  35089  usgrcyclgt2v  35494  subfacp1lem5  35547  erdsze2lem1  35566  cvmseu  35639  cvmliftlem11  35658  cvmlift3lem8  35689  cvmlift3lem9  35690  trer  36689  meran1  36784  lukshef-ax2  36788  ordcmp  36820  curryset  37443  currysetlem3  37446  bj-snsetex  37460  pibt2  37923  wl-nfeqfb  38051  phpreu  38115  poimirlem1  38132  poimirlem2  38133  poimirlem9  38140  poimirlem18  38149  poimirlem27  38158  poimirlem31  38162  poimirlem32  38163  mblfinlem2  38169  sdclem2  38253  ismtyhmeolem  38315  heiborlem10  38331  notornotel1  38606  mpobi123f  38673  lpssat  39649  lssatle  39651  lssat  39652  cdlemk45  41583  dia2dimlem9  41708  diblsmopel  41807  dochspss  42014  baerlem5blem2  42348  hdmap14lem4a  42507  lcmineqlem2  42659  aks6d1c1p2  42738  aks6d1c1p3  42739  hashscontpowcl  42749  hashscontpow  42751  aks6d1c4  42753  idomnnzpownz  42761  idomnnzgmulnz  42762  aks6d1c6lem3  42801  aks6d1c6lem5  42806  aks6d1c7lem1  42809  aomclem6  43648  kelac1  43652  kelac2  43654  isnumbasgrplem3  43694  proot1mul  43783  ntrclsk3  44658  neicvgel1  44707  ismnushort  44875  choicefi  45775  infleinflem1  45943  supcnvlimsup  46312  stoweidlem11  46583  stoweidlem14  46586  fourierdlem12  46691  fourierdlem51  46729  fourierdlem80  46758  smfresal  47360  simpcntrab  47442  natglobalincr  47451  adh-minim  47593  afv0nbfvbi  47743  iccelpart  48037  fmtnoprmfac2lem1  48173  perfectALTVlem1  48341  bgoldbtbndlem2  48426  cznabel  48880  mgpsumz  48993  uprcl2  49818  lanrcl  50250  ranrcl  50251