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  2738  2reu5  3704  relopabi  5778  f1ocnvfvrneq  7241  fcof1oinvd  7248  isoselem  7296  isose  7298  fnwelem  8081  tposss  8177  smoiso  8302  nneob  8592  difsnen  8997  php  9141  ordtypelem10  9442  oismo  9455  cantnflt2  9594  oemapso  9603  cantnf  9614  scott0  9810  tskwe  9874  infxpenlem  9935  ac10ct  9956  acndom  9973  dfac12lem2  10067  dfac12r  10069  pwdjudom  10137  ackbij1lem15  10155  ackbij2lem2  10161  ackbij2lem3  10162  ackbij2  10164  fin23lem22  10249  domtriomlem  10364  axdc3lem2  10373  sdomsdomcard  10482  fpwwe2lem8  10561  canthp1lem2  10576  pwfseqlem5  10586  xnn0lem1lt  13196  fzssp1  13521  fzosplitsnm1  13695  fzofzp1  13719  fzostep1  13741  fldiv4lem1div2uz2  13795  fsuppmapnn0fiublem  13952  fsuppmapnn0fiub  13953  bcm1k  14277  pfxccatpfx2  14699  revrev  14729  climuni  15514  isercolllem2  15628  isercoll  15630  serf0  15643  fsumparts  15769  hashiun  15785  isumsup2  15811  climcndslem1  15814  climcndslem2  15815  binomfallfaclem2  16005  2mulprm  16662  oddprm  16781  vdwmc  16949  prdsplusg  17421  prdsvsca  17423  imasdsval2  17480  catcone0  17653  sscpwex  17782  ssc2  17789  pmtrfv  19427  symgtrinv  19447  psgnprfval  19496  odcl2  19540  lsmmod  19650  efgsdmi  19707  gsumzinv  19920  ablfac1b  20047  pgpfac1lem1  20051  pgpfaclem2  20059  ablfaclem2  20063  ablfac  20065  srng0  20831  orngsqr  20843  orngmullt  20848  ofldtos  20850  rmodislmod  20925  znzrh2  21525  znf1o  21531  znhash  21538  znfld  21540  cygznlem3  21549  psgnevpmb  21567  ip2di  21621  mpofrlmd  21757  ascl0  21864  ascl1  21865  mpfsubrg  22089  gsumply1subr  22197  evls1gsumadd  22289  pf1subrg  22313  mpfpf1  22316  pf1mpf  22317  scmatsgrp1  22487  madutpos  22607  iscncl  23234  qtopcmap  23684  hmeores  23736  qtopf1  23781  fbssfi  23802  filssufil  23877  fmfnfmlem3  23921  clssubg  24074  tmsxms  24451  prdsxms  24495  metustfbas  24522  metuel2  24530  restmetu  24535  tngngp2  24617  nrginvrcn  24657  nmhmcn  25087  iscmet3  25260  minveclem3  25396  ovoliunlem2  25470  ismbf3d  25621  i1fd  25648  dvadd  25907  dvmul  25908  dvaddf  25909  dvco  25914  dvcof  25915  dvcnvlem  25943  dgrub  26199  plyremlem  26270  fta1lem  26273  fta1  26274  vieta1lem2  26277  plyexmo  26279  elaa  26282  ulmcau  26360  ulmdvlem3  26367  efabl  26514  relogbf  26755  ppinprm  27115  chtnprm  27117  dchrzrh1  27207  dchr1  27220  dchr1re  27226  dchrptlem1  27227  dchrpt  27230  dchrsum2  27231  dchrhash  27234  gausslemma2dlem0c  27321  gausslemma2dlem0e  27323  gausslemma2dlem0i  27327  gausslemma2dlem1a  27328  gausslemma2dlem7  27336  gausslemma2d  27337  rpvmasumlem  27450  rpvmasum2  27475  mudivsum  27493  nosepssdm  27650  nosupbnd2lem1  27679  nosupbnd2  27680  noinfbnd2lem1  27694  noetasuplem2  27698  noetasuplem3  27699  noetainflem2  27702  tgldimor  28570  f1otrg  28939  nbusgrvtxm1  29448  wlkp1lem2  29741  pthdlem1  29834  crctcshlem4  29888  crctcshwlkn0  29889  crctcshtrl  29891  wspthsnonn0vne  29985  eupth2eucrct  30287  eupthvdres  30305  eucrctshift  30313  eucrct2eupth1  30314  minvecolem3  30947  acunirnmpt2  32733  acunirnmpt2f  32734  fnpreimac  32743  symgfcoeu  33143  tocycfvres1  33171  tocycfvres2  33172  tocyc01  33179  cycpmconjslem1  33215  cycpmconjslem2  33216  archiabllem1a  33252  znfermltl  33426  qusrn  33469  ressply1invg  33629  ressply1sub  33630  ply1fermltl  33646  dimkerim  33771  fedgmullem2  33774  lvecendof1f1o  33777  evls1fldgencl  33814  algextdeglem5  33865  mdetlap  33976  locfinref  33985  ordtconnlem1  34068  pl1cn  34099  zrhunitpreima  34120  qqhnm  34134  qqhucn  34136  rrexttps  34150  ldgenpisyslem1  34307  ddemeas  34380  1stmbfm  34404  2ndmbfm  34405  omsval  34437  sitgclbn  34487  eulerpartgbij  34516  eulerpartlemgs2  34524  unveldomd  34559  probmeasb  34574  plymulx0  34691  signstres  34719  bnj1098  34926  usgrcyclgt2v  35313  subfacp1lem5  35366  erdsze2lem1  35385  cvmseu  35458  cvmliftlem11  35477  cvmlift3lem8  35508  cvmlift3lem9  35509  trer  36498  meran1  36593  lukshef-ax2  36597  ordcmp  36629  curryset  37253  currysetlem3  37256  bj-snsetex  37270  pibt2  37733  wl-nfeqfb  37861  phpreu  37925  poimirlem1  37942  poimirlem2  37943  poimirlem9  37950  poimirlem18  37959  poimirlem27  37968  poimirlem31  37972  poimirlem32  37973  mblfinlem2  37979  sdclem2  38063  ismtyhmeolem  38125  heiborlem10  38141  notornotel1  38416  mpobi123f  38483  lpssat  39459  lssatle  39461  lssat  39462  cdlemk45  41393  dia2dimlem9  41518  diblsmopel  41617  dochspss  41824  baerlem5blem2  42158  hdmap14lem4a  42317  lcmineqlem2  42469  aks6d1c1p2  42548  aks6d1c1p3  42549  hashscontpowcl  42559  hashscontpow  42561  aks6d1c4  42563  idomnnzpownz  42571  idomnnzgmulnz  42572  aks6d1c6lem3  42611  aks6d1c6lem5  42616  aks6d1c7lem1  42619  aomclem6  43487  kelac1  43491  kelac2  43493  isnumbasgrplem3  43533  proot1mul  43622  ntrclsk3  44497  neicvgel1  44546  ismnushort  44728  choicefi  45629  infleinflem1  45799  supcnvlimsup  46168  stoweidlem11  46439  stoweidlem14  46442  fourierdlem12  46547  fourierdlem48  46582  fourierdlem51  46585  fourierdlem80  46614  sssmf  47166  smfresal  47216  simpcntrab  47298  natglobalincr  47307  adh-minim  47449  afv0nbfvbi  47599  iccelpart  47893  fmtnoprmfac2lem1  48029  perfectALTVlem1  48197  bgoldbtbndlem2  48282  cznabel  48736  mgpsumz  48838  uprcl2  49664  lanrcl  50096  ranrcl  50097