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  2056  eqeq1d  2732  2reu5  3737  relopabi  5793  f1ocnvfvrneq  7268  fcof1oinvd  7275  isoselem  7323  isose  7325  fnwelem  8119  tposss  8215  smoiso  8340  nneob  8631  difsnen  9030  php  9184  ordtypelem10  9498  oismo  9511  cantnflt2  9644  oemapso  9653  cantnf  9664  scott0  9857  tskwe  9921  infxpenlem  9984  ac10ct  10005  acndom  10022  dfac12lem2  10116  dfac12r  10118  pwdjudom  10186  ackbij1lem15  10204  ackbij2lem2  10210  ackbij2lem3  10211  ackbij2  10213  fin23lem22  10298  domtriomlem  10413  axdc3lem2  10422  sdomsdomcard  10531  fpwwe2lem8  10609  canthp1lem2  10624  pwfseqlem5  10634  xnn0lem1lt  13217  fzssp1  13541  fzosplitsnm1  13713  fzofzp1  13737  fzostep1  13756  fldiv4lem1div2uz2  13810  fsuppmapnn0fiublem  13965  fsuppmapnn0fiub  13966  bcm1k  14290  pfxccatpfx2  14712  revrev  14742  climuni  15525  isercolllem2  15639  isercoll  15641  serf0  15654  fsumparts  15779  hashiun  15795  isumsup2  15819  climcndslem1  15822  climcndslem2  15823  binomfallfaclem2  16013  2mulprm  16669  oddprm  16787  vdwmc  16955  prdsplusg  17427  prdsvsca  17429  imasdsval2  17485  catcone0  17654  sscpwex  17783  ssc2  17790  pmtrfv  19388  symgtrinv  19408  psgnprfval  19457  odcl2  19501  lsmmod  19611  efgsdmi  19668  gsumzinv  19881  ablfac1b  20008  pgpfac1lem1  20012  pgpfaclem2  20020  ablfaclem2  20024  ablfac  20026  srng0  20769  rmodislmod  20842  znzrh2  21461  znf1o  21467  znhash  21474  znfld  21476  cygznlem3  21485  psgnevpmb  21502  ip2di  21556  mpofrlmd  21692  ascl0  21799  ascl1  21800  mpfsubrg  22016  gsumply1subr  22124  evls1gsumadd  22217  pf1subrg  22241  mpfpf1  22244  pf1mpf  22245  scmatsgrp1  22415  madutpos  22535  iscncl  23162  qtopcmap  23612  hmeores  23664  qtopf1  23709  fbssfi  23730  filssufil  23805  fmfnfmlem3  23849  clssubg  24002  tmsxms  24380  prdsxms  24424  metustfbas  24451  metuel2  24459  restmetu  24464  tngngp2  24546  nrginvrcn  24586  nmhmcn  25026  iscmet3  25200  minveclem3  25336  ovoliunlem2  25411  ismbf3d  25562  i1fd  25589  dvadd  25850  dvmul  25851  dvaddf  25852  dvco  25858  dvcof  25859  dvcnvlem  25887  dgrub  26146  plyremlem  26219  fta1lem  26222  fta1  26223  vieta1lem2  26226  plyexmo  26228  elaa  26231  ulmcau  26311  ulmdvlem3  26318  efabl  26466  relogbf  26708  ppinprm  27069  chtnprm  27071  dchrzrh1  27162  dchr1  27175  dchr1re  27181  dchrptlem1  27182  dchrpt  27185  dchrsum2  27186  dchrhash  27189  gausslemma2dlem0c  27276  gausslemma2dlem0e  27278  gausslemma2dlem0i  27282  gausslemma2dlem1a  27283  gausslemma2dlem7  27291  gausslemma2d  27292  rpvmasumlem  27405  rpvmasum2  27430  mudivsum  27448  nosepssdm  27605  nosupbnd2lem1  27634  nosupbnd2  27635  noinfbnd2lem1  27649  noetasuplem2  27653  noetasuplem3  27654  noetainflem2  27657  tgldimor  28436  f1otrg  28805  nbusgrvtxm1  29313  wlkp1lem2  29609  pthdlem1  29703  crctcshlem4  29757  crctcshwlkn0  29758  crctcshtrl  29760  wspthsnonn0vne  29854  eupth2eucrct  30153  eupthvdres  30171  eucrctshift  30179  eucrct2eupth1  30180  minvecolem3  30812  acunirnmpt2  32592  acunirnmpt2f  32593  fnpreimac  32603  symgfcoeu  33047  tocycfvres1  33075  tocycfvres2  33076  tocyc01  33083  cycpmconjslem1  33119  cycpmconjslem2  33120  archiabllem1a  33153  orngsqr  33290  orngmullt  33295  ofldtos  33297  znfermltl  33345  qusrn  33388  ressply1invg  33546  ressply1sub  33547  ply1fermltl  33561  dimkerim  33631  fedgmullem2  33634  lvecendof1f1o  33637  evls1fldgencl  33673  algextdeglem5  33719  mdetlap  33830  locfinref  33839  ordtconnlem1  33922  pl1cn  33953  zrhunitpreima  33974  qqhnm  33988  qqhucn  33990  rrexttps  34004  ldgenpisyslem1  34161  ddemeas  34234  1stmbfm  34259  2ndmbfm  34260  omsval  34292  sitgclbn  34342  eulerpartgbij  34371  eulerpartlemgs2  34379  unveldomd  34414  probmeasb  34429  plymulx0  34546  signstres  34574  bnj1098  34781  usgrcyclgt2v  35120  subfacp1lem5  35173  erdsze2lem1  35192  cvmseu  35265  cvmliftlem11  35284  cvmlift3lem8  35315  cvmlift3lem9  35316  trer  36301  meran1  36396  lukshef-ax2  36400  ordcmp  36432  curryset  36931  currysetlem3  36934  bj-snsetex  36948  pibt2  37402  wl-nfeqfb  37521  phpreu  37595  poimirlem1  37612  poimirlem2  37613  poimirlem9  37620  poimirlem18  37629  poimirlem27  37638  poimirlem31  37642  poimirlem32  37643  mblfinlem2  37649  sdclem2  37733  ismtyhmeolem  37795  heiborlem10  37811  notornotel1  38086  mpobi123f  38153  lpssat  38998  lssatle  39000  lssat  39001  cdlemk45  40933  dia2dimlem9  41058  diblsmopel  41157  dochspss  41364  baerlem5blem2  41698  hdmap14lem4a  41857  lcmineqlem2  42010  aks6d1c1p2  42089  aks6d1c1p3  42090  hashscontpowcl  42100  hashscontpow  42102  aks6d1c4  42104  idomnnzpownz  42112  idomnnzgmulnz  42113  aks6d1c6lem3  42152  aks6d1c6lem5  42157  aks6d1c7lem1  42160  aomclem6  43020  kelac1  43024  kelac2  43026  isnumbasgrplem3  43066  proot1mul  43155  ntrclsk3  44031  neicvgel1  44080  ismnushort  44262  choicefi  45166  infleinflem1  45339  supcnvlimsup  45711  stoweidlem11  45982  stoweidlem14  45985  fourierdlem12  46090  fourierdlem48  46125  fourierdlem51  46128  fourierdlem80  46157  sssmf  46709  smfresal  46759  simpcntrab  46841  natglobalincr  46848  adh-minim  46972  afv0nbfvbi  47122  iccelpart  47389  fmtnoprmfac2lem1  47522  perfectALTVlem1  47677  bgoldbtbndlem2  47762  cznabel  48177  mgpsumz  48279  uprcl2  49096  lanrcl  49497  ranrcl  49498