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  2089  eqeq1d  2762  2reu5  3715  relopabi  5799  f1ocnvfvrneq  7294  fcof1oinvd  7301  isoselem  7349  isose  7351  fnwelem  8145  tposss  8247  smoiso  8373  nneob  8668  difsnen  9081  php  9225  ordtypelem10  9524  oismo  9537  cantnflt2  9677  oemapso  9686  cantnf  9697  scott0b  9940  scott0OLD  9941  tskwe  10034  infxpenlem  10095  ac10ct  10116  acndom  10133  dfac12lem2  10226  dfac12r  10228  pwdjudom  10296  ackbij1lem15  10314  ackbij2lem2  10320  ackbij2lem3  10321  ackbij2  10323  fin23lem22  10408  domtriomlem  10523  axdc3lem2  10532  sdomsdomcard  10647  fpwwe2lem8  10726  canthp1lem2  10741  pwfseqlem5  10751  xnn0lem1lt  13377  fzssp1  13704  fzosplitsnm1  13878  fzofzp1  13902  fzostep1  13924  fldiv4lem1div2uz2  13979  fsuppmapnn0fiublem  14136  fsuppmapnn0fiub  14137  bcm1k  14462  pfxccatpfx2  14890  revrev  14920  climuni  15724  isercolllem2  15838  isercoll  15840  serf0  15853  fsumparts  15978  hashiun  15994  isumsup2  16020  climcndslem1  16023  climcndslem2  16024  binomfallfaclem2  16211  2mulprm  16873  oddprm  16993  vdwmc  17161  prdsplusg  17634  prdsvsca  17636  imasdsval2  17693  catcone0  17866  sscpwex  17995  ssc2  18002  pmtrfv  19671  symgtrinv  19691  psgnprfval  19740  odcl2  19784  lsmmod  19894  efgsdmi  19951  gsumzinv  20164  ablfac1b  20291  pgpfac1lem1  20295  pgpfaclem2  20303  ablfaclem2  20307  ablfac  20309  srng0  21116  orngsqr  21128  orngmullt  21133  ofldtos  21135  rmodislmod  21210  znzrh2  21856  znf1o  21862  znhash  21869  znfld  21871  cygznlem3  21880  psgnevpmb  21898  ip2di  21952  mpofrlmd  22088  ascl0  22197  ascl1  22198  mpfsubrg  22425  gsumply1subr  22556  evls1gsumadd  22647  pf1subrg  22671  mpfpf1  22674  pf1mpf  22675  scmatsgrp1  22842  madutpos  22962  iscncl  23592  qtopcmap  24043  hmeores  24095  qtopf1  24140  fbssfi  24161  filssufil  24236  fmfnfmlem3  24280  clssubg  24433  tmsxms  24810  prdsxms  24854  metustfbas  24881  metuel2  24889  restmetu  24894  tngngp2  24976  nrginvrcn  25016  nmhmcn  25446  iscmet3  25619  minveclem3  25755  ovoliunlem2  25829  ismbf3d  25980  i1fd  26007  dvadd  26265  dvmul  26266  dvaddf  26267  dvco  26272  dvcof  26273  dvcnvlem  26301  dgrub  26558  plyn0mulidp  26607  plyremlem  26630  fta1lem  26633  fta1  26634  vieta1lem2  26639  plyexmo  26641  elaa  26644  ulmcau  26727  ulmdvlem3  26734  efabl  26883  relogbf  27124  ppinprm  27484  chtnprm  27486  dchrzrh1  27576  dchr1  27589  dchr1re  27595  dchrptlem1  27596  dchrpt  27599  dchrsum2  27600  dchrhash  27603  gausslemma2dlem0c  27690  gausslemma2dlem0e  27692  gausslemma2dlem0i  27696  gausslemma2dlem1a  27697  gausslemma2dlem7  27705  gausslemma2d  27706  rpvmasumlem  27819  rpvmasum2  27844  mudivsum  27862  nosepssdm  28048  nosupbnd2lem1  28077  nosupbnd2  28078  noinfbnd2lem1  28092  noetasuplem2  28096  noetasuplem3  28097  noetainflem2  28100  tgldimor  28970  f1otrg  29453  nbusgrvtxm1  29965  wlkp1lem2  30258  pthdlem1  30357  crctcshlem4  30414  crctcshwlkn0  30415  crctcshtrl  30417  wspthsnonn0vne  30511  eupth2eucrct  30823  eupthvdres  30841  eucrctshift  30849  eucrct2eupth1  30850  minvecolem3  31483  acunirnmpt2  33301  acunirnmpt2f  33302  fnpreimac  33311  symgfcoeu  33689  tocycfvres1  33717  tocycfvres2  33718  tocyc01  33725  cycpmconjslem1  33761  cycpmconjslem2  33762  archiabllem1a  33798  znfermltl  33968  qusrn  34006  ressply1invg  34147  ressply1sub  34148  ply1fermltl  34164  dimkerim  34305  fedgmullem2  34308  lvecendof1f1o  34311  evls1fldgencl  34348  algextdeglem5  34399  mdetlap  34510  locfinref  34519  ordtconnlem1  34602  pl1cn  34633  zrhunitpreima  34654  qqhnm  34668  qqhucn  34670  rrexttps  34684  ldgenpisyslem1  34842  ddemeas  34915  1stmbfm  34938  2ndmbfm  34939  omsval  34971  sitgclbn  35021  eulerpartgbij  35050  eulerpartlemgs2  35058  unveldomd  35093  probmeasb  35108  signstres  35250  bnj1098  35460  dfscott3  35797  usgrcyclgt2v  35986  subfacp1lem5  36035  erdsze2lem1  36054  cvmseu  36127  cvmliftlem11  36146  cvmlift3lem8  36177  cvmlift3lem9  36178  trer  37196  meran1  37291  lukshef-ax2  37295  ordcmp  37327  curryset  37951  currysetlem3  37954  bj-snsetex  37968  wl-nfeqfb  38561  phpreu  38620  poimirlem1  38632  poimirlem2  38633  poimirlem9  38640  poimirlem18  38649  poimirlem27  38658  poimirlem31  38662  poimirlem32  38663  mblfinlem2  38669  sdclem2  38769  ismtyhmeolem  38831  heiborlem10  38847  notornotel1  39120  mpobi123f  39187  lpssat  40163  lssatle  40165  lssat  40166  cdlemk45  42097  dia2dimlem9  42222  diblsmopel  42321  dochspss  42528  baerlem5blem2  42862  hdmap14lem4a  43021  lcmineqlem2  43173  aks6d1c1p2  43252  aks6d1c1p3  43253  hashscontpowcl  43263  hashscontpow  43265  aks6d1c4  43267  idomnnzpownz  43275  idomnnzgmulnz  43276  aks6d1c6lem3  43315  aks6d1c6lem5  43320  aks6d1c7lem1  43323  aomclem6  44154  kelac1  44158  kelac2  44160  isnumbasgrplem3  44200  proot1mul  44289  ntrclsk3  45163  neicvgel1  45212  ismnushort  45378  hfxp  46110  choicefi  46307  infleinflem1  46474  supcnvlimsup  46843  stoweidlem11  47114  stoweidlem14  47117  fourierdlem12  47222  fourierdlem51  47260  fourierdlem80  47289  smfresal  47891  simpcntrab  47973  adh-minim  48164  afv0nbfvbi  48314  iccelpart  48608  fmtnoprmfac2lem1  48744  perfectALTVlem1  48912  bgoldbtbndlem2  48997  cznabel  49450  mgpsumz  49567  uprcl2  50398  lanrcl  50897  ranrcl  50898