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  2054  eqeq1d  2736  2reu5  3748  relopabi  5814  f1ocnvfvrneq  7289  fcof1oinvd  7296  isoselem  7344  isose  7346  fnwelem  8139  tposss  8235  wfrlem5OLD  8336  smoiso  8385  nneob  8677  difsnen  9076  php  9230  ordtypelem10  9550  oismo  9563  cantnflt2  9696  oemapso  9705  cantnf  9716  scott0  9909  tskwe  9973  infxpenlem  10036  ac10ct  10057  acndom  10074  dfac12lem2  10168  dfac12r  10170  pwdjudom  10238  ackbij1lem15  10256  ackbij2lem2  10262  ackbij2lem3  10263  ackbij2  10265  fin23lem22  10350  domtriomlem  10465  axdc3lem2  10474  sdomsdomcard  10583  fpwwe2lem8  10661  canthp1lem2  10676  pwfseqlem5  10686  xnn0lem1lt  13269  fzssp1  13590  fzosplitsnm1  13762  fzofzp1  13786  fzostep1  13805  fldiv4lem1div2uz2  13859  fsuppmapnn0fiublem  14014  fsuppmapnn0fiub  14015  bcm1k  14337  pfxccatpfx2  14758  revrev  14788  climuni  15571  isercolllem2  15685  isercoll  15687  serf0  15700  fsumparts  15825  hashiun  15841  isumsup2  15865  climcndslem1  15868  climcndslem2  15869  binomfallfaclem2  16059  2mulprm  16713  oddprm  16831  vdwmc  16999  prdsplusg  17479  prdsvsca  17481  imasdsval2  17537  catcone0  17706  sscpwex  17835  ssc2  17842  pmtrfv  19443  symgtrinv  19463  psgnprfval  19512  odcl2  19556  lsmmod  19666  efgsdmi  19723  gsumzinv  19936  ablfac1b  20063  pgpfac1lem1  20067  pgpfaclem2  20075  ablfaclem2  20079  ablfac  20081  srng0  20828  rmodislmod  20901  znzrh2  21531  znf1o  21537  znhash  21544  znfld  21546  cygznlem3  21555  psgnevpmb  21572  ip2di  21626  mpofrlmd  21764  ascl0  21871  ascl1  21872  mpfsubrg  22094  gsumply1subr  22202  evls1gsumadd  22295  pf1subrg  22319  mpfpf1  22322  pf1mpf  22323  scmatsgrp1  22495  madutpos  22615  iscncl  23242  qtopcmap  23692  hmeores  23744  qtopf1  23789  fbssfi  23810  filssufil  23885  fmfnfmlem3  23929  clssubg  24082  tmsxms  24462  prdsxms  24506  metustfbas  24533  metuel2  24541  restmetu  24546  tngngp2  24628  nrginvrcn  24668  nmhmcn  25108  iscmet3  25282  minveclem3  25418  ovoliunlem2  25493  ismbf3d  25644  i1fd  25671  dvadd  25932  dvmul  25933  dvaddf  25934  dvco  25940  dvcof  25941  dvcnvlem  25969  dgrub  26228  plyremlem  26301  fta1lem  26304  fta1  26305  vieta1lem2  26308  plyexmo  26310  elaa  26313  ulmcau  26393  ulmdvlem3  26400  efabl  26547  relogbf  26789  ppinprm  27150  chtnprm  27152  dchrzrh1  27243  dchr1  27256  dchr1re  27262  dchrptlem1  27263  dchrpt  27266  dchrsum2  27267  dchrhash  27270  gausslemma2dlem0c  27357  gausslemma2dlem0e  27359  gausslemma2dlem0i  27363  gausslemma2dlem1a  27364  gausslemma2dlem7  27372  gausslemma2d  27373  rpvmasumlem  27486  rpvmasum2  27511  mudivsum  27529  nosepssdm  27686  nosupbnd2lem1  27715  nosupbnd2  27716  noinfbnd2lem1  27730  noetasuplem2  27734  noetasuplem3  27735  noetainflem2  27738  tgldimor  28465  f1otrg  28834  nbusgrvtxm1  29343  wlkp1lem2  29639  pthdlem1  29733  crctcshlem4  29787  crctcshwlkn0  29788  crctcshtrl  29790  wspthsnonn0vne  29884  eupth2eucrct  30183  eupthvdres  30201  eucrctshift  30209  eucrct2eupth1  30210  minvecolem3  30842  acunirnmpt2  32617  acunirnmpt2f  32618  fnpreimac  32628  symgfcoeu  33048  tocycfvres1  33076  tocycfvres2  33077  tocyc01  33084  cycpmconjslem1  33120  cycpmconjslem2  33121  archiabllem1a  33144  orngsqr  33280  orngmullt  33285  ofldtos  33287  znfermltl  33335  qusrn  33378  ressply1invg  33535  ressply1sub  33536  ply1fermltl  33550  dimkerim  33619  fedgmullem2  33622  lvecendof1f1o  33625  evls1fldgencl  33661  algextdeglem5  33703  mdetlap  33772  locfinref  33781  ordtconnlem1  33864  pl1cn  33895  zrhunitpreima  33918  qqhnm  33932  qqhucn  33934  rrexttps  33948  ldgenpisyslem1  34105  ddemeas  34178  1stmbfm  34203  2ndmbfm  34204  omsval  34236  sitgclbn  34286  eulerpartgbij  34315  eulerpartlemgs2  34323  unveldomd  34358  probmeasb  34373  plymulx0  34503  signstres  34531  bnj1098  34738  usgrcyclgt2v  35077  subfacp1lem5  35130  erdsze2lem1  35149  cvmseu  35222  cvmliftlem11  35241  cvmlift3lem8  35272  cvmlift3lem9  35273  trer  36258  meran1  36353  lukshef-ax2  36357  ordcmp  36389  curryset  36888  currysetlem3  36891  bj-snsetex  36905  pibt2  37359  wl-nfeqfb  37478  phpreu  37552  poimirlem1  37569  poimirlem2  37570  poimirlem9  37577  poimirlem18  37586  poimirlem27  37595  poimirlem31  37599  poimirlem32  37600  mblfinlem2  37606  sdclem2  37690  ismtyhmeolem  37752  heiborlem10  37768  notornotel1  38043  mpobi123f  38110  lpssat  38955  lssatle  38957  lssat  38958  cdlemk45  40890  dia2dimlem9  41015  diblsmopel  41114  dochspss  41321  baerlem5blem2  41655  hdmap14lem4a  41814  lcmineqlem2  41972  aks6d1c1p2  42051  aks6d1c1p3  42052  hashscontpowcl  42062  hashscontpow  42064  aks6d1c4  42066  idomnnzpownz  42074  idomnnzgmulnz  42075  aks6d1c6lem3  42114  aks6d1c6lem5  42119  aks6d1c7lem1  42122  aomclem6  43016  kelac1  43020  kelac2  43022  isnumbasgrplem3  43062  proot1mul  43151  ntrclsk3  44028  neicvgel1  44077  ismnushort  44265  choicefi  45150  infleinflem1  45326  supcnvlimsup  45700  stoweidlem11  45971  stoweidlem14  45974  fourierdlem12  46079  fourierdlem48  46114  fourierdlem51  46117  fourierdlem80  46146  sssmf  46698  smfresal  46748  simpcntrab  46830  natglobalincr  46837  adh-minim  46959  afv0nbfvbi  47109  iccelpart  47366  fmtnoprmfac2lem1  47499  perfectALTVlem1  47654  bgoldbtbndlem2  47739  cznabel  48122  mgpsumz  48224  uprcl2  48900