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  2092  eqeq1d  2765  2reu5  3719  relopabiOLD  5806  f1ocnvfvrneq  7317  fcof1oinvd  7324  isoselem  7372  isose  7374  fnwelem  8170  tposss  8272  smoiso  8398  nneob  8693  difsnen  9106  php  9250  ordtypelem10  9548  oismo  9561  cantnflt2  9701  oemapso  9710  cantnf  9721  scott0b  9964  scott0OLD  9965  tskwe  10058  infxpenlem  10119  ac10ct  10140  acndom  10157  dfac12lem2  10250  dfac12r  10252  pwdjudom  10320  ackbij1lem15  10338  ackbij2lem2  10344  ackbij2lem3  10345  ackbij2  10347  fin23lem22  10432  domtriomlem  10547  axdc3lem2  10556  sdomsdomcard  10671  fpwwe2lem8  10750  canthp1lem2  10765  pwfseqlem5  10775  xnn0lem1lt  13401  fzssp1  13728  fzosplitsnm1  13902  fzofzp1  13926  fzostep1  13948  fldiv4lem1div2uz2  14003  fsuppmapnn0fiublem  14160  fsuppmapnn0fiub  14161  bcm1k  14486  pfxccatpfx2  14914  revrev  14944  climuni  15748  isercolllem2  15862  isercoll  15864  serf0  15877  fsumparts  16002  hashiun  16018  isumsup2  16044  climcndslem1  16047  climcndslem2  16048  binomfallfaclem2  16235  2mulprm  16897  oddprm  17017  vdwmc  17185  prdsplusg  17658  prdsvsca  17660  imasdsval2  17717  catcone0  17890  sscpwex  18019  ssc2  18026  pmtrfv  19696  symgtrinv  19716  psgnprfval  19765  odcl2  19809  lsmmod  19919  efgsdmi  19976  gsumzinv  20189  ablfac1b  20316  pgpfac1lem1  20320  pgpfaclem2  20328  ablfaclem2  20332  ablfac  20334  srng0  21141  orngsqr  21153  orngmullt  21158  ofldtos  21160  rmodislmod  21235  znzrh2  21881  znf1o  21887  znhash  21894  znfld  21896  cygznlem3  21905  psgnevpmb  21923  ip2di  21977  mpofrlmd  22113  ascl0  22222  ascl1  22223  mpfsubrg  22450  gsumply1subr  22581  evls1gsumadd  22672  pf1subrg  22696  mpfpf1  22699  pf1mpf  22700  scmatsgrp1  22867  madutpos  22987  iscncl  23617  qtopcmap  24068  hmeores  24120  qtopf1  24165  fbssfi  24186  filssufil  24261  fmfnfmlem3  24305  clssubg  24458  tmsxms  24835  prdsxms  24879  metustfbas  24906  metuel2  24914  restmetu  24919  tngngp2  25001  nrginvrcn  25041  nmhmcn  25471  iscmet3  25644  minveclem3  25780  ovoliunlem2  25854  ismbf3d  26005  i1fd  26032  dvadd  26290  dvmul  26291  dvaddf  26292  dvco  26297  dvcof  26298  dvcnvlem  26326  dgrub  26583  plyn0mulidp  26632  plyremlem  26655  fta1lem  26658  fta1  26659  vieta1lem2  26664  plyexmo  26666  elaa  26669  ulmcau  26752  ulmdvlem3  26759  efabl  26908  relogbf  27149  ppinprm  27509  chtnprm  27511  dchrzrh1  27601  dchr1  27614  dchr1re  27620  dchrptlem1  27621  dchrpt  27624  dchrsum2  27625  dchrhash  27628  gausslemma2dlem0c  27715  gausslemma2dlem0e  27717  gausslemma2dlem0i  27721  gausslemma2dlem1a  27722  gausslemma2dlem7  27730  gausslemma2d  27731  rpvmasumlem  27844  rpvmasum2  27869  mudivsum  27887  nosepssdm  28073  nosupbnd2lem1  28102  nosupbnd2  28103  noinfbnd2lem1  28117  noetasuplem2  28121  noetasuplem3  28122  noetainflem2  28125  tgldimor  28995  f1otrg  29478  nbusgrvtxm1  29990  wlkp1lem2  30283  pthdlem1  30382  crctcshlem4  30439  crctcshwlkn0  30440  crctcshtrl  30442  wspthsnonn0vne  30536  eupth2eucrct  30848  eupthvdres  30866  eucrctshift  30874  eucrct2eupth1  30875  minvecolem3  31508  acunirnmpt2  33326  acunirnmpt2f  33327  fnpreimac  33336  symgfcoeu  33713  tocycfvres1  33741  tocycfvres2  33742  tocyc01  33749  cycpmconjslem1  33785  cycpmconjslem2  33786  archiabllem1a  33822  znfermltl  33992  qusrn  34030  ressply1invg  34171  ressply1sub  34172  ply1fermltl  34188  dimkerim  34329  fedgmullem2  34332  lvecendof1f1o  34335  evls1fldgencl  34372  algextdeglem5  34423  mdetlap  34534  locfinref  34543  ordtconnlem1  34626  pl1cn  34657  zrhunitpreima  34678  qqhnm  34692  qqhucn  34694  rrexttps  34708  ldgenpisyslem1  34866  ddemeas  34939  1stmbfm  34962  2ndmbfm  34963  omsval  34995  sitgclbn  35045  eulerpartgbij  35074  eulerpartlemgs2  35082  unveldomd  35117  probmeasb  35132  signstres  35274  bnj1098  35484  dfscott3  35827  usgrcyclgt2v  36067  subfacp1lem5  36116  erdsze2lem1  36135  cvmseu  36208  cvmliftlem11  36227  cvmlift3lem8  36258  cvmlift3lem9  36259  trer  37282  meran1  37377  lukshef-ax2  37381  ordcmp  37413  curryset  38037  currysetlem3  38040  bj-snsetex  38054  wl-nfeqfb  38660  phpreu  38719  poimirlem1  38731  poimirlem2  38732  poimirlem9  38739  poimirlem18  38748  poimirlem27  38757  poimirlem31  38761  poimirlem32  38762  mblfinlem2  38768  sdclem2  38868  ismtyhmeolem  38930  heiborlem10  38946  notornotel1  39219  mpobi123f  39286  lpssat  40262  lssatle  40264  lssat  40265  cdlemk45  42196  dia2dimlem9  42321  diblsmopel  42420  dochspss  42627  baerlem5blem2  42961  hdmap14lem4a  43120  lcmineqlem2  43272  aks6d1c1p2  43351  aks6d1c1p3  43352  hashscontpowcl  43362  hashscontpow  43364  aks6d1c4  43366  idomnnzpownz  43374  idomnnzgmulnz  43375  aks6d1c6lem3  43414  aks6d1c6lem5  43419  aks6d1c7lem1  43422  aomclem6  44254  kelac1  44258  kelac2  44260  isnumbasgrplem3  44299  proot1mul  44388  ntrclsk3  45262  neicvgel1  45311  ismnushort  45477  hfxp  46212  choicefi  46419  infleinflem1  46586  supcnvlimsup  46955  stoweidlem11  47226  stoweidlem14  47229  fourierdlem12  47334  fourierdlem51  47372  fourierdlem80  47401  smfresal  48003  simpcntrab  48085  adh-minim  48276  afv0nbfvbi  48426  iccelpart  48720  fmtnoprmfac2lem1  48856  perfectALTVlem1  49024  bgoldbtbndlem2  49109  cznabel  49562  mgpsumz  49679  uprcl2  50510  lanrcl  51009  ranrcl  51010