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  2087  eqeq1d  2765  2reu5  3722  relopabi  5811  f1ocnvfvrneq  7286  fcof1oinvd  7293  isoselem  7341  isose  7343  fnwelem  8128  tposss  8224  smoiso  8350  nneob  8643  difsnen  9048  php  9192  ordtypelem10  9490  oismo  9503  cantnflt2  9643  oemapso  9652  cantnf  9663  scott0  9861  tskwe  9937  infxpenlem  9998  ac10ct  10019  acndom  10036  dfac12lem2  10129  dfac12r  10131  pwdjudom  10199  ackbij1lem15  10217  ackbij2lem2  10223  ackbij2lem3  10224  ackbij2  10226  fin23lem22  10312  domtriomlem  10427  axdc3lem2  10436  sdomsdomcard  10545  fpwwe2lem8  10624  canthp1lem2  10639  pwfseqlem5  10649  xnn0lem1lt  13271  fzssp1  13597  fzosplitsnm1  13771  fzofzp1  13795  fzostep1  13817  fldiv4lem1div2uz2  13871  fsuppmapnn0fiublem  14028  fsuppmapnn0fiub  14029  bcm1k  14353  pfxccatpfx2  14776  revrev  14806  climuni  15605  isercolllem2  15719  isercoll  15721  serf0  15734  fsumparts  15860  hashiun  15876  isumsup2  15902  climcndslem1  15905  climcndslem2  15906  binomfallfaclem2  16095  2mulprm  16752  oddprm  16871  vdwmc  17039  prdsplusg  17512  prdsvsca  17514  imasdsval2  17571  catcone0  17744  sscpwex  17873  ssc2  17880  pmtrfv  19523  symgtrinv  19543  psgnprfval  19592  odcl2  19636  lsmmod  19746  efgsdmi  19803  gsumzinv  20016  ablfac1b  20143  pgpfac1lem1  20147  pgpfaclem2  20155  ablfaclem2  20159  ablfac  20161  srng0  20938  orngsqr  20950  orngmullt  20955  ofldtos  20957  rmodislmod  21032  znzrh2  21676  znf1o  21682  znhash  21689  znfld  21691  cygznlem3  21700  psgnevpmb  21718  ip2di  21772  mpofrlmd  21908  ascl0  22015  ascl1  22016  mpfsubrg  22243  gsumply1subr  22374  evls1gsumadd  22465  pf1subrg  22489  mpfpf1  22492  pf1mpf  22493  scmatsgrp1  22660  madutpos  22780  iscncl  23407  qtopcmap  23857  hmeores  23909  qtopf1  23954  fbssfi  23975  filssufil  24050  fmfnfmlem3  24094  clssubg  24247  tmsxms  24624  prdsxms  24668  metustfbas  24695  metuel2  24703  restmetu  24708  tngngp2  24790  nrginvrcn  24830  nmhmcn  25260  iscmet3  25433  minveclem3  25569  ovoliunlem2  25643  ismbf3d  25794  i1fd  25821  dvadd  26080  dvmul  26081  dvaddf  26082  dvco  26087  dvcof  26088  dvcnvlem  26116  dgrub  26372  plyn0mulidp  26423  plyremlem  26446  fta1lem  26449  fta1  26450  vieta1lem2  26453  plyexmo  26455  elaa  26458  ulmcau  26536  ulmdvlem3  26543  efabl  26693  relogbf  26934  ppinprm  27294  chtnprm  27296  dchrzrh1  27386  dchr1  27399  dchr1re  27405  dchrptlem1  27406  dchrpt  27409  dchrsum2  27410  dchrhash  27413  gausslemma2dlem0c  27500  gausslemma2dlem0e  27502  gausslemma2dlem0i  27506  gausslemma2dlem1a  27507  gausslemma2dlem7  27515  gausslemma2d  27516  rpvmasumlem  27629  rpvmasum2  27654  mudivsum  27672  nosepssdm  27828  nosupbnd2lem1  27857  nosupbnd2  27858  noinfbnd2lem1  27872  noetasuplem2  27876  noetasuplem3  27877  noetainflem2  27880  tgldimor  28749  f1otrg  29198  nbusgrvtxm1  29707  wlkp1lem2  30000  pthdlem1  30093  crctcshlem4  30147  crctcshwlkn0  30148  crctcshtrl  30150  wspthsnonn0vne  30244  eupth2eucrct  30546  eupthvdres  30564  eucrctshift  30572  eucrct2eupth1  30573  minvecolem3  31206  acunirnmpt2  32983  acunirnmpt2f  32984  fnpreimac  32993  symgfcoeu  33380  tocycfvres1  33408  tocycfvres2  33409  tocyc01  33416  cycpmconjslem1  33452  cycpmconjslem2  33453  archiabllem1a  33489  znfermltl  33659  qusrn  33696  ressply1invg  33837  ressply1sub  33838  ply1fermltl  33854  dimkerim  33995  fedgmullem2  33998  lvecendof1f1o  34001  evls1fldgencl  34038  algextdeglem5  34089  mdetlap  34200  locfinref  34209  ordtconnlem1  34292  pl1cn  34323  zrhunitpreima  34344  qqhnm  34358  qqhucn  34360  rrexttps  34374  ldgenpisyslem1  34531  ddemeas  34604  1stmbfm  34628  2ndmbfm  34629  omsval  34661  sitgclbn  34711  eulerpartgbij  34740  eulerpartlemgs2  34748  unveldomd  34783  probmeasb  34798  signstres  34940  bnj1098  35150  dfscott3  35490  usgrcyclgt2v  35601  subfacp1lem5  35654  erdsze2lem1  35673  cvmseu  35746  cvmliftlem11  35765  cvmlift3lem8  35796  cvmlift3lem9  35797  trer  36805  meran1  36900  lukshef-ax2  36904  ordcmp  36936  curryset  37560  currysetlem3  37563  bj-snsetex  37577  pibt2  38041  wl-nfeqfb  38169  phpreu  38233  poimirlem1  38250  poimirlem2  38251  poimirlem9  38258  poimirlem18  38267  poimirlem27  38276  poimirlem31  38280  poimirlem32  38281  mblfinlem2  38287  sdclem2  38371  ismtyhmeolem  38433  heiborlem10  38449  notornotel1  38722  mpobi123f  38789  lpssat  39765  lssatle  39767  lssat  39768  cdlemk45  41699  dia2dimlem9  41824  diblsmopel  41923  dochspss  42130  baerlem5blem2  42464  hdmap14lem4a  42623  lcmineqlem2  42775  aks6d1c1p2  42854  aks6d1c1p3  42855  hashscontpowcl  42865  hashscontpow  42867  aks6d1c4  42869  idomnnzpownz  42877  idomnnzgmulnz  42878  aks6d1c6lem3  42917  aks6d1c6lem5  42922  aks6d1c7lem1  42925  aomclem6  43766  kelac1  43770  kelac2  43772  isnumbasgrplem3  43812  proot1mul  43901  ntrclsk3  44776  neicvgel1  44825  ismnushort  44991  choicefi  45897  infleinflem1  46065  supcnvlimsup  46434  stoweidlem11  46705  stoweidlem14  46708  fourierdlem12  46813  fourierdlem51  46851  fourierdlem80  46880  smfresal  47482  simpcntrab  47564  natglobalincr  47573  adh-minim  47715  afv0nbfvbi  47865  iccelpart  48159  fmtnoprmfac2lem1  48295  perfectALTVlem1  48463  bgoldbtbndlem2  48548  cznabel  49002  mgpsumz  49119  uprcl2  49944  lanrcl  50376  ranrcl  50377