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  2050  eqeq1d  2727  2reu5  3750  relopabi  5824  f1ocnvfvrneq  7295  fcof1oinvd  7302  isoselem  7348  isose  7350  fnwelem  8136  tposss  8233  wfrlem5OLD  8334  smoiso  8383  nneob  8677  difsnen  9081  php  9238  ordtypelem10  9557  oismo  9570  cantnflt2  9703  oemapso  9712  cantnf  9723  scott0  9916  tskwe  9980  infxpenlem  10043  ac10ct  10064  acndom  10081  dfac12lem2  10174  dfac12r  10176  pwdjudom  10246  ackbij1lem15  10264  ackbij2lem2  10270  ackbij2lem3  10271  ackbij2  10273  fin23lem22  10357  domtriomlem  10472  axdc3lem2  10481  sdomsdomcard  10590  fpwwe2lem8  10668  canthp1lem2  10683  pwfseqlem5  10693  xnn0lem1lt  13263  fzssp1  13584  fzosplitsnm1  13747  fzofzp1  13770  fzostep1  13789  fldiv4lem1div2uz2  13842  fsuppmapnn0fiublem  13996  fsuppmapnn0fiub  13997  bcm1k  14315  pfxccatpfx2  14728  revrev  14758  climuni  15537  isercolllem2  15653  isercoll  15655  serf0  15668  fsumparts  15793  hashiun  15809  isumsup2  15833  climcndslem1  15836  climcndslem2  15837  binomfallfaclem2  16025  2mulprm  16672  oddprm  16787  vdwmc  16955  prdsplusg  17448  prdsvsca  17450  imasdsval2  17506  catcone0  17675  sscpwex  17806  ssc2  17813  pmtrfv  19424  symgtrinv  19444  psgnprfval  19493  odcl2  19537  lsmmod  19647  efgsdmi  19704  gsumzinv  19917  ablfac1b  20044  pgpfac1lem1  20048  pgpfaclem2  20056  ablfaclem2  20060  ablfac  20062  srng0  20757  rmodislmod  20830  znzrh2  21501  znf1o  21507  znhash  21514  znfld  21516  cygznlem3  21525  psgnevpmb  21541  ip2di  21595  mpofrlmd  21733  ascl0  21839  ascl1  21840  mpfsubrg  22076  gsumply1subr  22181  evls1gsumadd  22273  pf1subrg  22297  mpfpf1  22300  pf1mpf  22301  scmatsgrp1  22473  madutpos  22593  iscncl  23222  qtopcmap  23672  hmeores  23724  qtopf1  23769  fbssfi  23790  filssufil  23865  fmfnfmlem3  23909  clssubg  24062  tmsxms  24444  prdsxms  24488  metustfbas  24515  metuel2  24523  restmetu  24528  tngngp2  24618  nrginvrcn  24658  nmhmcn  25096  iscmet3  25270  minveclem3  25406  ovoliunlem2  25481  ismbf3d  25632  i1fd  25659  dvadd  25920  dvmul  25921  dvaddf  25922  dvco  25928  dvcof  25929  dvcnvlem  25957  dgrub  26218  plyremlem  26289  fta1lem  26292  fta1  26293  vieta1lem2  26296  plyexmo  26298  elaa  26301  ulmcau  26381  ulmdvlem3  26388  efabl  26534  relogbf  26773  ppinprm  27134  chtnprm  27136  dchrzrh1  27227  dchr1  27240  dchr1re  27246  dchrptlem1  27247  dchrpt  27250  dchrsum2  27251  dchrhash  27254  gausslemma2dlem0c  27341  gausslemma2dlem0e  27343  gausslemma2dlem0i  27347  gausslemma2dlem1a  27348  gausslemma2dlem7  27356  gausslemma2d  27357  rpvmasumlem  27470  rpvmasum2  27495  mudivsum  27513  nosepssdm  27670  nosupbnd2lem1  27699  nosupbnd2  27700  noinfbnd2lem1  27714  noetasuplem2  27718  noetasuplem3  27719  noetainflem2  27722  tgldimor  28383  f1otrg  28752  nbusgrvtxm1  29269  wlkp1lem2  29565  pthdlem1  29657  crctcshlem4  29708  crctcshwlkn0  29709  crctcshtrl  29711  wspthsnonn0vne  29805  eupth2eucrct  30104  eupthvdres  30122  eucrctshift  30130  eucrct2eupth1  30131  minvecolem3  30763  acunirnmpt2  32532  acunirnmpt2f  32533  fnpreimac  32543  symgfcoeu  32900  tocycfvres1  32928  tocycfvres2  32929  tocyc01  32936  cycpmconjslem1  32972  cycpmconjslem2  32973  archiabllem1a  32996  orngsqr  33123  orngmullt  33128  ofldtos  33130  znfermltl  33182  qusrn  33226  ressply1invg  33383  ressply1sub  33384  ply1fermltl  33395  dimkerim  33458  fedgmullem2  33461  evls1fldgencl  33491  algextdeglem5  33522  mdetlap  33566  locfinref  33575  ordtconnlem1  33658  pl1cn  33689  zrhunitpreima  33712  qqhnm  33724  qqhucn  33726  rrexttps  33740  ldgenpisyslem1  33915  ddemeas  33988  1stmbfm  34013  2ndmbfm  34014  omsval  34046  sitgclbn  34096  eulerpartgbij  34125  eulerpartlemgs2  34133  unveldomd  34168  probmeasb  34183  plymulx0  34312  signstres  34340  bnj1098  34547  usgrcyclgt2v  34874  subfacp1lem5  34927  erdsze2lem1  34946  cvmseu  35019  cvmliftlem11  35038  cvmlift3lem8  35069  cvmlift3lem9  35070  trer  35933  meran1  36028  lukshef-ax2  36032  ordcmp  36064  curryset  36558  currysetlem3  36561  bj-snsetex  36575  pibt2  37029  wl-nfeqfb  37136  phpreu  37210  poimirlem1  37227  poimirlem2  37228  poimirlem9  37235  poimirlem18  37244  poimirlem27  37253  poimirlem31  37257  poimirlem32  37258  mblfinlem2  37264  sdclem2  37348  ismtyhmeolem  37410  heiborlem10  37426  notornotel1  37701  mpobi123f  37768  lpssat  38617  lssatle  38619  lssat  38620  cdlemk45  40552  dia2dimlem9  40677  diblsmopel  40776  dochspss  40983  baerlem5blem2  41317  hdmap14lem4a  41476  lcmineqlem2  41635  aks6d1c1p2  41714  aks6d1c1p3  41715  hashscontpowcl  41725  hashscontpow  41727  aks6d1c4  41729  idomnnzpownz  41737  idomnnzgmulnz  41738  aks6d1c6lem3  41777  aks6d1c6lem5  41782  aks6d1c7lem1  41785  aomclem6  42627  kelac1  42631  kelac2  42633  isnumbasgrplem3  42673  proot1mul  42766  ntrclsk3  43644  neicvgel1  43693  ismnushort  43882  choicefi  44714  infleinflem1  44892  supcnvlimsup  45268  stoweidlem11  45539  stoweidlem14  45542  fourierdlem12  45647  fourierdlem48  45682  fourierdlem51  45685  fourierdlem80  45714  sssmf  46266  smfresal  46316  simpcntrab  46398  natglobalincr  46403  adh-minim  46523  afv0nbfvbi  46671  iccelpart  46912  fmtnoprmfac2lem1  47045  perfectALTVlem1  47200  bgoldbtbndlem2  47285  cznabel  47510  mgpsumz  47614