Theorem 4syl 19

Description: Inference chaining three syllogisms syl 17. (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 18	. 2 ⊢ (𝜑 → 𝜃)
5		4syl.4	. 2 ⊢ (𝜃 → 𝜏)
6	4, 5	syl 17	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  2059  eqeq1d  2739  2reu5  3705  relopabi  5771  f1ocnvfvrneq  7234  fcof1oinvd  7241  isoselem  7289  isose  7291  fnwelem  8074  tposss  8170  smoiso  8295  nneob  8585  difsnen  8990  php  9134  ordtypelem10  9435  oismo  9448  cantnflt2  9585  oemapso  9594  cantnf  9605  scott0  9801  tskwe  9865  infxpenlem  9926  ac10ct  9947  acndom  9964  dfac12lem2  10058  dfac12r  10060  pwdjudom  10128  ackbij1lem15  10146  ackbij2lem2  10152  ackbij2lem3  10153  ackbij2  10155  fin23lem22  10240  domtriomlem  10355  axdc3lem2  10364  sdomsdomcard  10473  fpwwe2lem8  10552  canthp1lem2  10567  pwfseqlem5  10577  xnn0lem1lt  13187  fzssp1  13512  fzosplitsnm1  13686  fzofzp1  13710  fzostep1  13732  fldiv4lem1div2uz2  13786  fsuppmapnn0fiublem  13943  fsuppmapnn0fiub  13944  bcm1k  14268  pfxccatpfx2  14690  revrev  14720  climuni  15505  isercolllem2  15619  isercoll  15621  serf0  15634  fsumparts  15760  hashiun  15776  isumsup2  15802  climcndslem1  15805  climcndslem2  15806  binomfallfaclem2  15996  2mulprm  16653  oddprm  16772  vdwmc  16940  prdsplusg  17412  prdsvsca  17414  imasdsval2  17471  catcone0  17644  sscpwex  17773  ssc2  17780  pmtrfv  19418  symgtrinv  19438  psgnprfval  19487  odcl2  19531  lsmmod  19641  efgsdmi  19698  gsumzinv  19911  ablfac1b  20038  pgpfac1lem1  20042  pgpfaclem2  20050  ablfaclem2  20054  ablfac  20056  srng0  20822  orngsqr  20834  orngmullt  20839  ofldtos  20841  rmodislmod  20916  znzrh2  21535  znf1o  21541  znhash  21548  znfld  21550  cygznlem3  21559  psgnevpmb  21577  ip2di  21631  mpofrlmd  21767  ascl0  21874  ascl1  21875  mpfsubrg  22099  gsumply1subr  22207  evls1gsumadd  22299  pf1subrg  22323  mpfpf1  22326  pf1mpf  22327  scmatsgrp1  22497  madutpos  22617  iscncl  23244  qtopcmap  23694  hmeores  23746  qtopf1  23791  fbssfi  23812  filssufil  23887  fmfnfmlem3  23931  clssubg  24084  tmsxms  24461  prdsxms  24505  metustfbas  24532  metuel2  24540  restmetu  24545  tngngp2  24627  nrginvrcn  24667  nmhmcn  25097  iscmet3  25270  minveclem3  25406  ovoliunlem2  25480  ismbf3d  25631  i1fd  25658  dvadd  25917  dvmul  25918  dvaddf  25919  dvco  25924  dvcof  25925  dvcnvlem  25953  dgrub  26209  plyremlem  26281  fta1lem  26284  fta1  26285  vieta1lem2  26288  plyexmo  26290  elaa  26293  ulmcau  26373  ulmdvlem3  26380  efabl  26527  relogbf  26768  ppinprm  27129  chtnprm  27131  dchrzrh1  27221  dchr1  27234  dchr1re  27240  dchrptlem1  27241  dchrpt  27244  dchrsum2  27245  dchrhash  27248  gausslemma2dlem0c  27335  gausslemma2dlem0e  27337  gausslemma2dlem0i  27341  gausslemma2dlem1a  27342  gausslemma2dlem7  27350  gausslemma2d  27351  rpvmasumlem  27464  rpvmasum2  27489  mudivsum  27507  nosepssdm  27664  nosupbnd2lem1  27693  nosupbnd2  27694  noinfbnd2lem1  27708  noetasuplem2  27712  noetasuplem3  27713  noetainflem2  27716  tgldimor  28584  f1otrg  28953  nbusgrvtxm1  29462  wlkp1lem2  29756  pthdlem1  29849  crctcshlem4  29903  crctcshwlkn0  29904  crctcshtrl  29906  wspthsnonn0vne  30000  eupth2eucrct  30302  eupthvdres  30320  eucrctshift  30328  eucrct2eupth1  30329  minvecolem3  30962  acunirnmpt2  32748  acunirnmpt2f  32749  fnpreimac  32758  symgfcoeu  33158  tocycfvres1  33186  tocycfvres2  33187  tocyc01  33194  cycpmconjslem1  33230  cycpmconjslem2  33231  archiabllem1a  33267  znfermltl  33441  qusrn  33484  ressply1invg  33644  ressply1sub  33645  ply1fermltl  33661  dimkerim  33787  fedgmullem2  33790  lvecendof1f1o  33793  evls1fldgencl  33830  algextdeglem5  33881  mdetlap  33992  locfinref  34001  ordtconnlem1  34084  pl1cn  34115  zrhunitpreima  34136  qqhnm  34150  qqhucn  34152  rrexttps  34166  ldgenpisyslem1  34323  ddemeas  34396  1stmbfm  34420  2ndmbfm  34421  omsval  34453  sitgclbn  34503  eulerpartgbij  34532  eulerpartlemgs2  34540  unveldomd  34575  probmeasb  34590  plymulx0  34707  signstres  34735  bnj1098  34942  usgrcyclgt2v  35329  subfacp1lem5  35382  erdsze2lem1  35401  cvmseu  35474  cvmliftlem11  35493  cvmlift3lem8  35524  cvmlift3lem9  35525  trer  36514  meran1  36609  lukshef-ax2  36613  ordcmp  36645  curryset  37269  currysetlem3  37272  bj-snsetex  37286  pibt2  37747  wl-nfeqfb  37875  phpreu  37939  poimirlem1  37956  poimirlem2  37957  poimirlem9  37964  poimirlem18  37973  poimirlem27  37982  poimirlem31  37986  poimirlem32  37987  mblfinlem2  37993  sdclem2  38077  ismtyhmeolem  38139  heiborlem10  38155  notornotel1  38430  mpobi123f  38497  lpssat  39473  lssatle  39475  lssat  39476  cdlemk45  41407  dia2dimlem9  41532  diblsmopel  41631  dochspss  41838  baerlem5blem2  42172  hdmap14lem4a  42331  lcmineqlem2  42483  aks6d1c1p2  42562  aks6d1c1p3  42563  hashscontpowcl  42573  hashscontpow  42575  aks6d1c4  42577  idomnnzpownz  42585  idomnnzgmulnz  42586  aks6d1c6lem3  42625  aks6d1c6lem5  42630  aks6d1c7lem1  42633  aomclem6  43505  kelac1  43509  kelac2  43511  isnumbasgrplem3  43551  proot1mul  43640  ntrclsk3  44515  neicvgel1  44564  ismnushort  44746  choicefi  45647  infleinflem1  45817  supcnvlimsup  46186  stoweidlem11  46457  stoweidlem14  46460  fourierdlem12  46565  fourierdlem48  46600  fourierdlem51  46603  fourierdlem80  46632  sssmf  47184  smfresal  47234  simpcntrab  47316  natglobalincr  47323  adh-minim  47461  afv0nbfvbi  47611  iccelpart  47905  fmtnoprmfac2lem1  48041  perfectALTVlem1  48209  bgoldbtbndlem2  48294  cznabel  48748  mgpsumz  48850  uprcl2  49676  lanrcl  50108  ranrcl  50109