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  2055  eqeq1d  2742  2reu5  3780  relopabi  5846  f1ocnvfvrneq  7322  fcof1oinvd  7329  isoselem  7377  isose  7379  fnwelem  8172  tposss  8268  wfrlem5OLD  8369  smoiso  8418  nneob  8712  difsnen  9119  php  9273  ordtypelem10  9596  oismo  9609  cantnflt2  9742  oemapso  9751  cantnf  9762  scott0  9955  tskwe  10019  infxpenlem  10082  ac10ct  10103  acndom  10120  dfac12lem2  10214  dfac12r  10216  pwdjudom  10284  ackbij1lem15  10302  ackbij2lem2  10308  ackbij2lem3  10309  ackbij2  10311  fin23lem22  10396  domtriomlem  10511  axdc3lem2  10520  sdomsdomcard  10629  fpwwe2lem8  10707  canthp1lem2  10722  pwfseqlem5  10732  xnn0lem1lt  13306  fzssp1  13627  fzosplitsnm1  13791  fzofzp1  13814  fzostep1  13833  fldiv4lem1div2uz2  13887  fsuppmapnn0fiublem  14041  fsuppmapnn0fiub  14042  bcm1k  14364  pfxccatpfx2  14785  revrev  14815  climuni  15598  isercolllem2  15714  isercoll  15716  serf0  15729  fsumparts  15854  hashiun  15870  isumsup2  15894  climcndslem1  15897  climcndslem2  15898  binomfallfaclem2  16088  2mulprm  16740  oddprm  16857  vdwmc  17025  prdsplusg  17518  prdsvsca  17520  imasdsval2  17576  catcone0  17745  sscpwex  17876  ssc2  17883  pmtrfv  19494  symgtrinv  19514  psgnprfval  19563  odcl2  19607  lsmmod  19717  efgsdmi  19774  gsumzinv  19987  ablfac1b  20114  pgpfac1lem1  20118  pgpfaclem2  20126  ablfaclem2  20130  ablfac  20132  srng0  20877  rmodislmod  20950  znzrh2  21587  znf1o  21593  znhash  21600  znfld  21602  cygznlem3  21611  psgnevpmb  21628  ip2di  21682  mpofrlmd  21820  ascl0  21927  ascl1  21928  mpfsubrg  22150  gsumply1subr  22256  evls1gsumadd  22349  pf1subrg  22373  mpfpf1  22376  pf1mpf  22377  scmatsgrp1  22549  madutpos  22669  iscncl  23298  qtopcmap  23748  hmeores  23800  qtopf1  23845  fbssfi  23866  filssufil  23941  fmfnfmlem3  23985  clssubg  24138  tmsxms  24520  prdsxms  24564  metustfbas  24591  metuel2  24599  restmetu  24604  tngngp2  24694  nrginvrcn  24734  nmhmcn  25172  iscmet3  25346  minveclem3  25482  ovoliunlem2  25557  ismbf3d  25708  i1fd  25735  dvadd  25997  dvmul  25998  dvaddf  25999  dvco  26005  dvcof  26006  dvcnvlem  26034  dgrub  26293  plyremlem  26364  fta1lem  26367  fta1  26368  vieta1lem2  26371  plyexmo  26373  elaa  26376  ulmcau  26456  ulmdvlem3  26463  efabl  26610  relogbf  26852  ppinprm  27213  chtnprm  27215  dchrzrh1  27306  dchr1  27319  dchr1re  27325  dchrptlem1  27326  dchrpt  27329  dchrsum2  27330  dchrhash  27333  gausslemma2dlem0c  27420  gausslemma2dlem0e  27422  gausslemma2dlem0i  27426  gausslemma2dlem1a  27427  gausslemma2dlem7  27435  gausslemma2d  27436  rpvmasumlem  27549  rpvmasum2  27574  mudivsum  27592  nosepssdm  27749  nosupbnd2lem1  27778  nosupbnd2  27779  noinfbnd2lem1  27793  noetasuplem2  27797  noetasuplem3  27798  noetainflem2  27801  tgldimor  28528  f1otrg  28897  nbusgrvtxm1  29414  wlkp1lem2  29710  pthdlem1  29802  crctcshlem4  29853  crctcshwlkn0  29854  crctcshtrl  29856  wspthsnonn0vne  29950  eupth2eucrct  30249  eupthvdres  30267  eucrctshift  30275  eucrct2eupth1  30276  minvecolem3  30908  acunirnmpt2  32678  acunirnmpt2f  32679  fnpreimac  32689  symgfcoeu  33075  tocycfvres1  33103  tocycfvres2  33104  tocyc01  33111  cycpmconjslem1  33147  cycpmconjslem2  33148  archiabllem1a  33171  orngsqr  33299  orngmullt  33304  ofldtos  33306  znfermltl  33359  qusrn  33402  ressply1invg  33559  ressply1sub  33560  ply1fermltl  33574  dimkerim  33640  fedgmullem2  33643  lvecendof1f1o  33646  evls1fldgencl  33680  algextdeglem5  33712  mdetlap  33778  locfinref  33787  ordtconnlem1  33870  pl1cn  33901  zrhunitpreima  33924  qqhnm  33936  qqhucn  33938  rrexttps  33952  ldgenpisyslem1  34127  ddemeas  34200  1stmbfm  34225  2ndmbfm  34226  omsval  34258  sitgclbn  34308  eulerpartgbij  34337  eulerpartlemgs2  34345  unveldomd  34380  probmeasb  34395  plymulx0  34524  signstres  34552  bnj1098  34759  usgrcyclgt2v  35099  subfacp1lem5  35152  erdsze2lem1  35171  cvmseu  35244  cvmliftlem11  35263  cvmlift3lem8  35294  cvmlift3lem9  35295  trer  36282  meran1  36377  lukshef-ax2  36381  ordcmp  36413  curryset  36912  currysetlem3  36915  bj-snsetex  36929  pibt2  37383  wl-nfeqfb  37490  phpreu  37564  poimirlem1  37581  poimirlem2  37582  poimirlem9  37589  poimirlem18  37598  poimirlem27  37607  poimirlem31  37611  poimirlem32  37612  mblfinlem2  37618  sdclem2  37702  ismtyhmeolem  37764  heiborlem10  37780  notornotel1  38055  mpobi123f  38122  lpssat  38969  lssatle  38971  lssat  38972  cdlemk45  40904  dia2dimlem9  41029  diblsmopel  41128  dochspss  41335  baerlem5blem2  41669  hdmap14lem4a  41828  lcmineqlem2  41987  aks6d1c1p2  42066  aks6d1c1p3  42067  hashscontpowcl  42077  hashscontpow  42079  aks6d1c4  42081  idomnnzpownz  42089  idomnnzgmulnz  42090  aks6d1c6lem3  42129  aks6d1c6lem5  42134  aks6d1c7lem1  42137  aomclem6  43016  kelac1  43020  kelac2  43022  isnumbasgrplem3  43062  proot1mul  43155  ntrclsk3  44032  neicvgel1  44081  ismnushort  44270  choicefi  45107  infleinflem1  45285  supcnvlimsup  45661  stoweidlem11  45932  stoweidlem14  45935  fourierdlem12  46040  fourierdlem48  46075  fourierdlem51  46078  fourierdlem80  46107  sssmf  46659  smfresal  46709  simpcntrab  46791  natglobalincr  46796  adh-minim  46916  afv0nbfvbi  47066  iccelpart  47307  fmtnoprmfac2lem1  47440  perfectALTVlem1  47595  bgoldbtbndlem2  47680  cznabel  47983  mgpsumz  48087