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  2058  eqeq1d  2735  2reu5  3713  relopabi  5766  f1ocnvfvrneq  7226  fcof1oinvd  7233  isoselem  7281  isose  7283  fnwelem  8067  tposss  8163  smoiso  8288  nneob  8577  difsnen  8979  php  9123  ordtypelem10  9420  oismo  9433  cantnflt2  9570  oemapso  9579  cantnf  9590  scott0  9786  tskwe  9850  infxpenlem  9911  ac10ct  9932  acndom  9949  dfac12lem2  10043  dfac12r  10045  pwdjudom  10113  ackbij1lem15  10131  ackbij2lem2  10137  ackbij2lem3  10138  ackbij2  10140  fin23lem22  10225  domtriomlem  10340  axdc3lem2  10349  sdomsdomcard  10458  fpwwe2lem8  10536  canthp1lem2  10551  pwfseqlem5  10561  xnn0lem1lt  13145  fzssp1  13469  fzosplitsnm1  13642  fzofzp1  13666  fzostep1  13688  fldiv4lem1div2uz2  13742  fsuppmapnn0fiublem  13899  fsuppmapnn0fiub  13900  bcm1k  14224  pfxccatpfx2  14646  revrev  14676  climuni  15461  isercolllem2  15575  isercoll  15577  serf0  15590  fsumparts  15715  hashiun  15731  isumsup2  15755  climcndslem1  15758  climcndslem2  15759  binomfallfaclem2  15949  2mulprm  16606  oddprm  16724  vdwmc  16892  prdsplusg  17364  prdsvsca  17366  imasdsval2  17422  catcone0  17595  sscpwex  17724  ssc2  17731  pmtrfv  19366  symgtrinv  19386  psgnprfval  19435  odcl2  19479  lsmmod  19589  efgsdmi  19646  gsumzinv  19859  ablfac1b  19986  pgpfac1lem1  19990  pgpfaclem2  19998  ablfaclem2  20002  ablfac  20004  srng0  20771  orngsqr  20783  orngmullt  20788  ofldtos  20790  rmodislmod  20865  znzrh2  21484  znf1o  21490  znhash  21497  znfld  21499  cygznlem3  21508  psgnevpmb  21526  ip2di  21580  mpofrlmd  21716  ascl0  21823  ascl1  21824  mpfsubrg  22039  gsumply1subr  22147  evls1gsumadd  22240  pf1subrg  22264  mpfpf1  22267  pf1mpf  22268  scmatsgrp1  22438  madutpos  22558  iscncl  23185  qtopcmap  23635  hmeores  23687  qtopf1  23732  fbssfi  23753  filssufil  23828  fmfnfmlem3  23872  clssubg  24025  tmsxms  24402  prdsxms  24446  metustfbas  24473  metuel2  24481  restmetu  24486  tngngp2  24568  nrginvrcn  24608  nmhmcn  25048  iscmet3  25221  minveclem3  25357  ovoliunlem2  25432  ismbf3d  25583  i1fd  25610  dvadd  25871  dvmul  25872  dvaddf  25873  dvco  25879  dvcof  25880  dvcnvlem  25908  dgrub  26167  plyremlem  26240  fta1lem  26243  fta1  26244  vieta1lem2  26247  plyexmo  26249  elaa  26252  ulmcau  26332  ulmdvlem3  26339  efabl  26487  relogbf  26729  ppinprm  27090  chtnprm  27092  dchrzrh1  27183  dchr1  27196  dchr1re  27202  dchrptlem1  27203  dchrpt  27206  dchrsum2  27207  dchrhash  27210  gausslemma2dlem0c  27297  gausslemma2dlem0e  27299  gausslemma2dlem0i  27303  gausslemma2dlem1a  27304  gausslemma2dlem7  27312  gausslemma2d  27313  rpvmasumlem  27426  rpvmasum2  27451  mudivsum  27469  nosepssdm  27626  nosupbnd2lem1  27655  nosupbnd2  27656  noinfbnd2lem1  27670  noetasuplem2  27674  noetasuplem3  27675  noetainflem2  27678  tgldimor  28481  f1otrg  28850  nbusgrvtxm1  29359  wlkp1lem2  29653  pthdlem1  29746  crctcshlem4  29800  crctcshwlkn0  29801  crctcshtrl  29803  wspthsnonn0vne  29897  eupth2eucrct  30199  eupthvdres  30217  eucrctshift  30225  eucrct2eupth1  30226  minvecolem3  30858  acunirnmpt2  32644  acunirnmpt2f  32645  fnpreimac  32655  symgfcoeu  33058  tocycfvres1  33086  tocycfvres2  33087  tocyc01  33094  cycpmconjslem1  33130  cycpmconjslem2  33131  archiabllem1a  33167  znfermltl  33338  qusrn  33381  ressply1invg  33539  ressply1sub  33540  ply1fermltl  33555  dimkerim  33661  fedgmullem2  33664  lvecendof1f1o  33667  evls1fldgencl  33704  algextdeglem5  33755  mdetlap  33866  locfinref  33875  ordtconnlem1  33958  pl1cn  33989  zrhunitpreima  34010  qqhnm  34024  qqhucn  34026  rrexttps  34040  ldgenpisyslem1  34197  ddemeas  34270  1stmbfm  34294  2ndmbfm  34295  omsval  34327  sitgclbn  34377  eulerpartgbij  34406  eulerpartlemgs2  34414  unveldomd  34449  probmeasb  34464  plymulx0  34581  signstres  34609  bnj1098  34816  usgrcyclgt2v  35196  subfacp1lem5  35249  erdsze2lem1  35268  cvmseu  35341  cvmliftlem11  35360  cvmlift3lem8  35391  cvmlift3lem9  35392  trer  36381  meran1  36476  lukshef-ax2  36480  ordcmp  36512  curryset  37011  currysetlem3  37014  bj-snsetex  37028  pibt2  37482  wl-nfeqfb  37601  phpreu  37665  poimirlem1  37682  poimirlem2  37683  poimirlem9  37690  poimirlem18  37699  poimirlem27  37708  poimirlem31  37712  poimirlem32  37713  mblfinlem2  37719  sdclem2  37803  ismtyhmeolem  37865  heiborlem10  37881  notornotel1  38156  mpobi123f  38223  lpssat  39133  lssatle  39135  lssat  39136  cdlemk45  41067  dia2dimlem9  41192  diblsmopel  41291  dochspss  41498  baerlem5blem2  41832  hdmap14lem4a  41991  lcmineqlem2  42144  aks6d1c1p2  42223  aks6d1c1p3  42224  hashscontpowcl  42234  hashscontpow  42236  aks6d1c4  42238  idomnnzpownz  42246  idomnnzgmulnz  42247  aks6d1c6lem3  42286  aks6d1c6lem5  42291  aks6d1c7lem1  42294  aomclem6  43177  kelac1  43181  kelac2  43183  isnumbasgrplem3  43223  proot1mul  43312  ntrclsk3  44188  neicvgel1  44237  ismnushort  44419  choicefi  45322  infleinflem1  45493  supcnvlimsup  45863  stoweidlem11  46134  stoweidlem14  46137  fourierdlem12  46242  fourierdlem48  46277  fourierdlem51  46280  fourierdlem80  46309  sssmf  46861  smfresal  46911  simpcntrab  46993  natglobalincr  47000  adh-minim  47126  afv0nbfvbi  47276  iccelpart  47558  fmtnoprmfac2lem1  47691  perfectALTVlem1  47846  bgoldbtbndlem2  47931  cznabel  48385  mgpsumz  48487  uprcl2  49315  lanrcl  49747  ranrcl  49748