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  2731  2reu5  3720  relopabi  5769  f1ocnvfvrneq  7227  fcof1oinvd  7234  isoselem  7282  isose  7284  fnwelem  8071  tposss  8167  smoiso  8292  nneob  8581  difsnen  8983  php  9131  ordtypelem10  9438  oismo  9451  cantnflt2  9588  oemapso  9597  cantnf  9608  scott0  9801  tskwe  9865  infxpenlem  9926  ac10ct  9947  acndom  9964  dfac12lem2  10058  dfac12r  10060  pwdjudom  10128  ackbij1lem15  10146  ackbij2lem2  10152  ackbij2lem3  10153  ackbij2  10155  fin23lem22  10240  domtriomlem  10355  axdc3lem2  10364  sdomsdomcard  10473  fpwwe2lem8  10551  canthp1lem2  10566  pwfseqlem5  10576  xnn0lem1lt  13164  fzssp1  13488  fzosplitsnm1  13661  fzofzp1  13685  fzostep1  13704  fldiv4lem1div2uz2  13758  fsuppmapnn0fiublem  13915  fsuppmapnn0fiub  13916  bcm1k  14240  pfxccatpfx2  14661  revrev  14691  climuni  15477  isercolllem2  15591  isercoll  15593  serf0  15606  fsumparts  15731  hashiun  15747  isumsup2  15771  climcndslem1  15774  climcndslem2  15775  binomfallfaclem2  15965  2mulprm  16622  oddprm  16740  vdwmc  16908  prdsplusg  17380  prdsvsca  17382  imasdsval2  17438  catcone0  17611  sscpwex  17740  ssc2  17747  pmtrfv  19349  symgtrinv  19369  psgnprfval  19418  odcl2  19462  lsmmod  19572  efgsdmi  19629  gsumzinv  19842  ablfac1b  19969  pgpfac1lem1  19973  pgpfaclem2  19981  ablfaclem2  19985  ablfac  19987  srng0  20757  orngsqr  20769  orngmullt  20774  ofldtos  20776  rmodislmod  20851  znzrh2  21470  znf1o  21476  znhash  21483  znfld  21485  cygznlem3  21494  psgnevpmb  21512  ip2di  21566  mpofrlmd  21702  ascl0  21809  ascl1  21810  mpfsubrg  22026  gsumply1subr  22134  evls1gsumadd  22227  pf1subrg  22251  mpfpf1  22254  pf1mpf  22255  scmatsgrp1  22425  madutpos  22545  iscncl  23172  qtopcmap  23622  hmeores  23674  qtopf1  23719  fbssfi  23740  filssufil  23815  fmfnfmlem3  23859  clssubg  24012  tmsxms  24390  prdsxms  24434  metustfbas  24461  metuel2  24469  restmetu  24474  tngngp2  24556  nrginvrcn  24596  nmhmcn  25036  iscmet3  25209  minveclem3  25345  ovoliunlem2  25420  ismbf3d  25571  i1fd  25598  dvadd  25859  dvmul  25860  dvaddf  25861  dvco  25867  dvcof  25868  dvcnvlem  25896  dgrub  26155  plyremlem  26228  fta1lem  26231  fta1  26232  vieta1lem2  26235  plyexmo  26237  elaa  26240  ulmcau  26320  ulmdvlem3  26327  efabl  26475  relogbf  26717  ppinprm  27078  chtnprm  27080  dchrzrh1  27171  dchr1  27184  dchr1re  27190  dchrptlem1  27191  dchrpt  27194  dchrsum2  27195  dchrhash  27198  gausslemma2dlem0c  27285  gausslemma2dlem0e  27287  gausslemma2dlem0i  27291  gausslemma2dlem1a  27292  gausslemma2dlem7  27300  gausslemma2d  27301  rpvmasumlem  27414  rpvmasum2  27439  mudivsum  27457  nosepssdm  27614  nosupbnd2lem1  27643  nosupbnd2  27644  noinfbnd2lem1  27658  noetasuplem2  27662  noetasuplem3  27663  noetainflem2  27666  tgldimor  28465  f1otrg  28834  nbusgrvtxm1  29342  wlkp1lem2  29636  pthdlem1  29729  crctcshlem4  29783  crctcshwlkn0  29784  crctcshtrl  29786  wspthsnonn0vne  29880  eupth2eucrct  30179  eupthvdres  30197  eucrctshift  30205  eucrct2eupth1  30206  minvecolem3  30838  acunirnmpt2  32617  acunirnmpt2f  32618  fnpreimac  32628  symgfcoeu  33037  tocycfvres1  33065  tocycfvres2  33066  tocyc01  33073  cycpmconjslem1  33109  cycpmconjslem2  33110  archiabllem1a  33146  znfermltl  33316  qusrn  33359  ressply1invg  33517  ressply1sub  33518  ply1fermltl  33532  dimkerim  33602  fedgmullem2  33605  lvecendof1f1o  33608  evls1fldgencl  33644  algextdeglem5  33690  mdetlap  33801  locfinref  33810  ordtconnlem1  33893  pl1cn  33924  zrhunitpreima  33945  qqhnm  33959  qqhucn  33961  rrexttps  33975  ldgenpisyslem1  34132  ddemeas  34205  1stmbfm  34230  2ndmbfm  34231  omsval  34263  sitgclbn  34313  eulerpartgbij  34342  eulerpartlemgs2  34350  unveldomd  34385  probmeasb  34400  plymulx0  34517  signstres  34545  bnj1098  34752  usgrcyclgt2v  35106  subfacp1lem5  35159  erdsze2lem1  35178  cvmseu  35251  cvmliftlem11  35270  cvmlift3lem8  35301  cvmlift3lem9  35302  trer  36292  meran1  36387  lukshef-ax2  36391  ordcmp  36423  curryset  36922  currysetlem3  36925  bj-snsetex  36939  pibt2  37393  wl-nfeqfb  37512  phpreu  37586  poimirlem1  37603  poimirlem2  37604  poimirlem9  37611  poimirlem18  37620  poimirlem27  37629  poimirlem31  37633  poimirlem32  37634  mblfinlem2  37640  sdclem2  37724  ismtyhmeolem  37786  heiborlem10  37802  notornotel1  38077  mpobi123f  38144  lpssat  38994  lssatle  38996  lssat  38997  cdlemk45  40929  dia2dimlem9  41054  diblsmopel  41153  dochspss  41360  baerlem5blem2  41694  hdmap14lem4a  41853  lcmineqlem2  42006  aks6d1c1p2  42085  aks6d1c1p3  42086  hashscontpowcl  42096  hashscontpow  42098  aks6d1c4  42100  idomnnzpownz  42108  idomnnzgmulnz  42109  aks6d1c6lem3  42148  aks6d1c6lem5  42153  aks6d1c7lem1  42156  aomclem6  43035  kelac1  43039  kelac2  43041  isnumbasgrplem3  43081  proot1mul  43170  ntrclsk3  44046  neicvgel1  44095  ismnushort  44277  choicefi  45181  infleinflem1  45353  supcnvlimsup  45725  stoweidlem11  45996  stoweidlem14  45999  fourierdlem12  46104  fourierdlem48  46139  fourierdlem51  46142  fourierdlem80  46171  sssmf  46723  smfresal  46773  simpcntrab  46855  natglobalincr  46862  adh-minim  46989  afv0nbfvbi  47139  iccelpart  47421  fmtnoprmfac2lem1  47554  perfectALTVlem1  47709  bgoldbtbndlem2  47794  cznabel  48248  mgpsumz  48350  uprcl2  49178  lanrcl  49610  ranrcl  49611