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  2768  2reu5  3724  relopabi  5814  f1ocnvfvrneq  7295  fcof1oinvd  7302  isoselem  7350  isose  7352  fnwelem  8136  tposss  8232  smoiso  8358  nneob  8651  difsnen  9057  php  9201  ordtypelem10  9499  oismo  9512  cantnflt2  9652  oemapso  9661  cantnf  9672  scott0b  9876  scott0OLD  9877  tskwe  9955  infxpenlem  10016  ac10ct  10037  acndom  10054  dfac12lem2  10147  dfac12r  10149  pwdjudom  10217  ackbij1lem15  10235  ackbij2lem2  10241  ackbij2lem3  10242  ackbij2  10244  fin23lem22  10329  domtriomlem  10444  axdc3lem2  10453  sdomsdomcard  10562  fpwwe2lem8  10641  canthp1lem2  10656  pwfseqlem5  10666  xnn0lem1lt  13288  fzssp1  13614  fzosplitsnm1  13788  fzofzp1  13812  fzostep1  13834  fldiv4lem1div2uz2  13889  fsuppmapnn0fiublem  14046  fsuppmapnn0fiub  14047  bcm1k  14371  pfxccatpfx2  14798  revrev  14828  climuni  15629  isercolllem2  15743  isercoll  15745  serf0  15758  fsumparts  15884  hashiun  15900  isumsup2  15926  climcndslem1  15929  climcndslem2  15930  binomfallfaclem2  16119  2mulprm  16776  oddprm  16895  vdwmc  17063  prdsplusg  17536  prdsvsca  17538  imasdsval2  17595  catcone0  17768  sscpwex  17897  ssc2  17904  pmtrfv  19553  symgtrinv  19573  psgnprfval  19622  odcl2  19666  lsmmod  19776  efgsdmi  19833  gsumzinv  20046  ablfac1b  20173  pgpfac1lem1  20177  pgpfaclem2  20185  ablfaclem2  20189  ablfac  20191  srng0  20994  orngsqr  21006  orngmullt  21011  ofldtos  21013  rmodislmod  21088  znzrh2  21732  znf1o  21738  znhash  21745  znfld  21747  cygznlem3  21756  psgnevpmb  21774  ip2di  21828  mpofrlmd  21964  ascl0  22071  ascl1  22072  mpfsubrg  22299  gsumply1subr  22430  evls1gsumadd  22521  pf1subrg  22545  mpfpf1  22548  pf1mpf  22549  scmatsgrp1  22716  madutpos  22836  iscncl  23463  qtopcmap  23913  hmeores  23965  qtopf1  24010  fbssfi  24031  filssufil  24106  fmfnfmlem3  24150  clssubg  24303  tmsxms  24680  prdsxms  24724  metustfbas  24751  metuel2  24759  restmetu  24764  tngngp2  24846  nrginvrcn  24886  nmhmcn  25316  iscmet3  25489  minveclem3  25625  ovoliunlem2  25699  ismbf3d  25850  i1fd  25877  dvadd  26136  dvmul  26137  dvaddf  26138  dvco  26143  dvcof  26144  dvcnvlem  26172  dgrub  26428  plyn0mulidp  26479  plyremlem  26502  fta1lem  26505  fta1  26506  vieta1lem2  26509  plyexmo  26511  elaa  26514  ulmcau  26595  ulmdvlem3  26602  efabl  26752  relogbf  26993  ppinprm  27353  chtnprm  27355  dchrzrh1  27445  dchr1  27458  dchr1re  27464  dchrptlem1  27465  dchrpt  27468  dchrsum2  27469  dchrhash  27472  gausslemma2dlem0c  27559  gausslemma2dlem0e  27561  gausslemma2dlem0i  27565  gausslemma2dlem1a  27566  gausslemma2dlem7  27574  gausslemma2d  27575  rpvmasumlem  27688  rpvmasum2  27713  mudivsum  27731  nosepssdm  27887  nosupbnd2lem1  27916  nosupbnd2  27917  noinfbnd2lem1  27931  noetasuplem2  27935  noetasuplem3  27936  noetainflem2  27939  tgldimor  28808  f1otrg  29257  nbusgrvtxm1  29766  wlkp1lem2  30059  pthdlem1  30152  crctcshlem4  30206  crctcshwlkn0  30207  crctcshtrl  30209  wspthsnonn0vne  30303  eupth2eucrct  30605  eupthvdres  30623  eucrctshift  30631  eucrct2eupth1  30632  minvecolem3  31265  acunirnmpt2  33042  acunirnmpt2f  33043  fnpreimac  33052  symgfcoeu  33433  tocycfvres1  33461  tocycfvres2  33462  tocyc01  33469  cycpmconjslem1  33505  cycpmconjslem2  33506  archiabllem1a  33542  znfermltl  33712  qusrn  33749  ressply1invg  33890  ressply1sub  33891  ply1fermltl  33907  dimkerim  34048  fedgmullem2  34051  lvecendof1f1o  34054  evls1fldgencl  34091  algextdeglem5  34142  mdetlap  34253  locfinref  34262  ordtconnlem1  34345  pl1cn  34376  zrhunitpreima  34397  qqhnm  34411  qqhucn  34413  rrexttps  34427  ldgenpisyslem1  34585  ddemeas  34658  1stmbfm  34682  2ndmbfm  34683  omsval  34715  sitgclbn  34765  eulerpartgbij  34794  eulerpartlemgs2  34802  unveldomd  34837  probmeasb  34852  signstres  34994  bnj1098  35204  dfscott3  35537  usgrcyclgt2v  35644  subfacp1lem5  35697  erdsze2lem1  35716  cvmseu  35789  cvmliftlem11  35808  cvmlift3lem8  35839  cvmlift3lem9  35840  trer  36868  meran1  36963  lukshef-ax2  36967  ordcmp  36999  curryset  37623  currysetlem3  37626  bj-snsetex  37640  pibt2  38104  wl-nfeqfb  38232  phpreu  38296  poimirlem1  38313  poimirlem2  38314  poimirlem9  38321  poimirlem18  38330  poimirlem27  38339  poimirlem31  38343  poimirlem32  38344  mblfinlem2  38350  sdclem2  38434  ismtyhmeolem  38496  heiborlem10  38512  notornotel1  38785  mpobi123f  38852  lpssat  39828  lssatle  39830  lssat  39831  cdlemk45  41762  dia2dimlem9  41887  diblsmopel  41986  dochspss  42193  baerlem5blem2  42527  hdmap14lem4a  42686  lcmineqlem2  42838  aks6d1c1p2  42917  aks6d1c1p3  42918  hashscontpowcl  42928  hashscontpow  42930  aks6d1c4  42932  idomnnzpownz  42940  idomnnzgmulnz  42941  aks6d1c6lem3  42980  aks6d1c6lem5  42985  aks6d1c7lem1  42988  aomclem6  43827  kelac1  43831  kelac2  43833  isnumbasgrplem3  43873  proot1mul  43962  ntrclsk3  44837  neicvgel1  44886  ismnushort  45052  choicefi  45958  infleinflem1  46126  supcnvlimsup  46495  stoweidlem11  46766  stoweidlem14  46769  fourierdlem12  46874  fourierdlem51  46912  fourierdlem80  46941  smfresal  47543  simpcntrab  47625  natglobalincr  47634  adh-minim  47779  afv0nbfvbi  47929  iccelpart  48223  fmtnoprmfac2lem1  48359  perfectALTVlem1  48527  bgoldbtbndlem2  48612  cznabel  49066  mgpsumz  49183  uprcl2  50008  lanrcl  50440  ranrcl  50441