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 ⊢ (𝜑 → 𝜏)

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  aevlem  2090  eqeq1d  2763  2reu5  3716  relopabi  5800  f1ocnvfvrneq  7286  fcof1oinvd  7293  isoselem  7341  isose  7343  fnwelem  8132  tposss  8228  smoiso  8354  nneob  8649  difsnen  9062  php  9206  ordtypelem10  9505  oismo  9518  cantnflt2  9658  oemapso  9667  cantnf  9678  scott0b  9918  scott0OLD  9919  tskwe  10012  infxpenlem  10073  ac10ct  10094  acndom  10111  dfac12lem2  10204  dfac12r  10206  pwdjudom  10274  ackbij1lem15  10292  ackbij2lem2  10298  ackbij2lem3  10299  ackbij2  10301  fin23lem22  10386  domtriomlem  10501  axdc3lem2  10510  sdomsdomcard  10625  fpwwe2lem8  10704  canthp1lem2  10719  pwfseqlem5  10729  xnn0lem1lt  13355  fzssp1  13681  fzosplitsnm1  13855  fzofzp1  13879  fzostep1  13901  fldiv4lem1div2uz2  13956  fsuppmapnn0fiublem  14113  fsuppmapnn0fiub  14114  bcm1k  14439  pfxccatpfx2  14866  revrev  14896  climuni  15699  isercolllem2  15813  isercoll  15815  serf0  15828  fsumparts  15953  hashiun  15969  isumsup2  15995  climcndslem1  15998  climcndslem2  15999  binomfallfaclem2  16186  2mulprm  16848  oddprm  16968  vdwmc  17136  prdsplusg  17609  prdsvsca  17611  imasdsval2  17668  catcone0  17841  sscpwex  17970  ssc2  17977  pmtrfv  19646  symgtrinv  19666  psgnprfval  19715  odcl2  19759  lsmmod  19869  efgsdmi  19926  gsumzinv  20139  ablfac1b  20266  pgpfac1lem1  20270  pgpfaclem2  20278  ablfaclem2  20282  ablfac  20284  srng0  21091  orngsqr  21103  orngmullt  21108  ofldtos  21110  rmodislmod  21185  znzrh2  21831  znf1o  21837  znhash  21844  znfld  21846  cygznlem3  21855  psgnevpmb  21873  ip2di  21927  mpofrlmd  22063  ascl0  22172  ascl1  22173  mpfsubrg  22400  gsumply1subr  22531  evls1gsumadd  22622  pf1subrg  22646  mpfpf1  22649  pf1mpf  22650  scmatsgrp1  22817  madutpos  22937  iscncl  23567  qtopcmap  24018  hmeores  24070  qtopf1  24115  fbssfi  24136  filssufil  24211  fmfnfmlem3  24255  clssubg  24408  tmsxms  24785  prdsxms  24829  metustfbas  24856  metuel2  24864  restmetu  24869  tngngp2  24951  nrginvrcn  24991  nmhmcn  25421  iscmet3  25594  minveclem3  25730  ovoliunlem2  25804  ismbf3d  25955  i1fd  25982  dvadd  26240  dvmul  26241  dvaddf  26242  dvco  26247  dvcof  26248  dvcnvlem  26276  dgrub  26533  plyn0mulidp  26584  plyremlem  26607  fta1lem  26610  fta1  26611  vieta1lem2  26616  plyexmo  26618  elaa  26621  ulmcau  26704  ulmdvlem3  26711  efabl  26860  relogbf  27101  ppinprm  27461  chtnprm  27463  dchrzrh1  27553  dchr1  27566  dchr1re  27572  dchrptlem1  27573  dchrpt  27576  dchrsum2  27577  dchrhash  27580  gausslemma2dlem0c  27667  gausslemma2dlem0e  27669  gausslemma2dlem0i  27673  gausslemma2dlem1a  27674  gausslemma2dlem7  27682  gausslemma2d  27683  rpvmasumlem  27796  rpvmasum2  27821  mudivsum  27839  nosepssdm  28025  nosupbnd2lem1  28054  nosupbnd2  28055  noinfbnd2lem1  28069  noetasuplem2  28073  noetasuplem3  28074  noetainflem2  28077  tgldimor  28947  f1otrg  29430  nbusgrvtxm1  29942  wlkp1lem2  30235  pthdlem1  30334  crctcshlem4  30391  crctcshwlkn0  30392  crctcshtrl  30394  wspthsnonn0vne  30488  eupth2eucrct  30800  eupthvdres  30818  eucrctshift  30826  eucrct2eupth1  30827  minvecolem3  31460  acunirnmpt2  33236  acunirnmpt2f  33237  fnpreimac  33246  symgfcoeu  33625  tocycfvres1  33653  tocycfvres2  33654  tocyc01  33661  cycpmconjslem1  33697  cycpmconjslem2  33698  archiabllem1a  33734  znfermltl  33904  qusrn  33942  ressply1invg  34083  ressply1sub  34084  ply1fermltl  34100  dimkerim  34241  fedgmullem2  34244  lvecendof1f1o  34247  evls1fldgencl  34284  algextdeglem5  34335  mdetlap  34446  locfinref  34455  ordtconnlem1  34538  pl1cn  34569  zrhunitpreima  34590  qqhnm  34604  qqhucn  34606  rrexttps  34620  ldgenpisyslem1  34778  ddemeas  34851  1stmbfm  34875  2ndmbfm  34876  omsval  34908  sitgclbn  34958  eulerpartgbij  34987  eulerpartlemgs2  34995  unveldomd  35030  probmeasb  35045  signstres  35187  bnj1098  35397  dfscott3  35721  usgrcyclgt2v  35879  subfacp1lem5  35918  erdsze2lem1  35937  cvmseu  36010  cvmliftlem11  36029  cvmlift3lem8  36060  cvmlift3lem9  36061  trer  37074  meran1  37169  lukshef-ax2  37173  ordcmp  37205  curryset  37829  currysetlem3  37832  bj-snsetex  37846  pibt2  38308  wl-nfeqfb  38436  phpreu  38495  poimirlem1  38507  poimirlem2  38508  poimirlem9  38515  poimirlem18  38524  poimirlem27  38533  poimirlem31  38537  poimirlem32  38538  mblfinlem2  38544  sdclem2  38644  ismtyhmeolem  38706  heiborlem10  38722  notornotel1  38995  mpobi123f  39062  lpssat  40038  lssatle  40040  lssat  40041  cdlemk45  41972  dia2dimlem9  42097  diblsmopel  42196  dochspss  42403  baerlem5blem2  42737  hdmap14lem4a  42896  lcmineqlem2  43048  aks6d1c1p2  43127  aks6d1c1p3  43128  hashscontpowcl  43138  hashscontpow  43140  aks6d1c4  43142  idomnnzpownz  43150  idomnnzgmulnz  43151  aks6d1c6lem3  43190  aks6d1c6lem5  43195  aks6d1c7lem1  43198  aomclem6  44019  kelac1  44023  kelac2  44025  isnumbasgrplem3  44065  proot1mul  44154  ntrclsk3  45029  neicvgel1  45078  ismnushort  45244  hfxp  45969  choicefi  46157  infleinflem1  46325  supcnvlimsup  46694  stoweidlem11  46965  stoweidlem14  46968  fourierdlem12  47073  fourierdlem51  47111  fourierdlem80  47140  smfresal  47742  simpcntrab  47824  adh-minim  48015  afv0nbfvbi  48165  iccelpart  48459  fmtnoprmfac2lem1  48595  perfectALTVlem1  48763  bgoldbtbndlem2  48848  cznabel  49301  mgpsumz  49418  uprcl2  50241  lanrcl  50673  ranrcl  50674