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 "minimize" command to have very long run times. However, feel free to use "minimize 4syl /override" if you wish. Remember to update the Travis "discouraged" file if it gets used. (New usage is discouraged.)

Hypotheses

Ref	Expression
4syl.1	|- ( ph -> ps )
4syl.2	|- ( ps -> ch )
4syl.3	|- ( ch -> th )
4syl.4	|- ( th -> ta )

Assertion

Ref	Expression
4syl	|- ( ph -> ta )

Proof of Theorem 4syl

Step	Hyp	Ref	Expression
1		4syl.1	. . 3 |- ( ph -> ps )
2		4syl.2	. . 3 |- ( ps -> ch )
3		4syl.3	. . 3 |- ( ch -> th )
4	1, 2, 3	3syl 18	. 2 |- ( ph -> th )
5		4syl.4	. 2 |- ( th -> ta )
6	4, 5	syl 17	1 |- ( ph -> ta )

Syntax hints:   -> wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  aevlem1  2022  aevlem1ALT  2154  eqeq1d  2453  2reu5  3248  f1ocnvfvrneq  6184  isoselem  6232  isose  6234  fnwelem  6911  tposss  6974  wfrlem5  7040  smoiso  7081  nneob  7353  difsnen  7654  ordtypelem10  8042  oismo  8055  cantnflt2  8178  oemapso  8187  cantnf  8198  scott0  8357  tskwe  8384  infxpenlem  8444  ac10ct  8465  acndom  8482  dfac12lem2  8574  dfac12r  8576  pwcdadom  8646  ackbij1lem15  8664  ackbij2lem2  8670  ackbij2lem3  8671  ackbij2  8673  fin23lem22  8757  domtriomlem  8872  axdc3lem2  8881  sdomsdomcard  8985  canthp1lem2  9078  pwfseqlem5  9088  gchhar  9104  fzssp1  11841  fzosplitsnm1  11988  fzofzp1  12008  fzostep1  12021  bcm1k  12500  swrdccat2  12814  revccat  12871  revrev  12872  climuni  13616  isercolllem2  13729  isercoll  13731  serf0  13747  fsumparts  13866  hashiun  13882  isumsup2  13904  climcndslem1  13907  climcndslem2  13908  binomfallfaclem2  14093  oddprm  14765  vdwmc  14928  prdsplusg  15356  prdsvsca  15358  imasdsval2  15417  imasdsval2OLD  15429  sscpwex  15720  ssc2  15727  pmtrfv  17093  symgtrinv  17113  odcl2  17216  lsmmod  17325  efgsdmi  17382  gsumzinv  17578  ablfac1b  17703  pgpfac1lem1  17707  pgpfaclem2  17715  ablfaclem2  17719  ablfac  17721  srng0  18088  mpfsubrg  18755  pf1subrg  18936  mpfpf1  18939  pf1mpf  18940  znzrh2  19116  znf1o  19122  znhash  19129  znfld  19131  cygznlem3  19140  ip2di  19208  iscncl  20285  qtopcmap  20734  hmeores  20786  qtopf1  20831  fbssfi  20852  filssufil  20927  fmfnfmlem3  20971  clssubg  21123  tmsxms  21501  prdsxms  21545  metustfbas  21572  metuel2  21580  restmetu  21585  nrginvrcn  21694  nmhmcn  22134  iscmet3  22263  minveclem3  22371  minveclem3OLD  22383  ovoliunlem2  22456  ismbf3d  22610  i1fd  22639  dvadd  22894  dvmul  22895  dvaddf  22896  dvco  22901  dvcof  22902  dvcnvlem  22928  mdeglt  23014  dgrub  23188  plyremlem  23257  fta1lem  23260  fta1  23261  vieta1lem2  23264  plyexmo  23266  elaa  23269  ulmcau  23350  ulmdvlem3  23357  ppinprm  24079  chtnprm  24081  dchrzrh1  24172  dchr1  24185  dchr1re  24191  dchrptlem1  24192  dchrpt  24195  dchrsum2  24196  dchrhash  24199  rpvmasumlem  24325  rpvmasum2  24350  mudivsum  24368  f1otrg  24901  cyclnspth  25359  el2spthonot  25598  usgravd0nedg  25646  subgores  26032  rngosn  26132  minvecolem3  26518  minvecolem3OLD  26528  acunirnmpt2  28262  acunirnmpt2f  28263  orngmullt  28572  locfinref  28668  pl1cn  28761  zrhunitpreima  28782  qqhnm  28794  qqhucn  28796  ldgenpisyslem1  28985  ddemeas  29059  1stmbfm  29082  2ndmbfm  29083  omsval  29117  omsvalOLD  29121  unveldomd  29248  probmeasb  29263  signstfvp  29460  signstres  29464  bnj1098  29595  subfacp1lem5  29907  erdsze2lem1  29926  cvmseu  29999  cvmliftlem11  30018  cvmlift3lem8  30049  cvmlift3lem9  30050  ghomfo  30309  frrlem5  30518  trer  30972  meran1  31071  lukshef-ax2  31075  ordcmp  31107  bj-aevlem1v  31352  wl-nfeqfb  31870  phpreu  31929  poimirlem1  31941  poimirlem9  31949  poimirlem31  31971  poimirlem32  31972  mblfinlem2  31978  sdclem2  32071  ismtyhmeolem  32136  heiborlem10  32152  lpssat  32579  lssatle  32581  lssat  32582  cdlemk45  34514  dia2dimlem9  34640  diblsmopel  34739  dochspss  34946  baerlem5blem2  35280  hdmap14lem4a  35442  aomclem6  35917  kelac1  35921  kelac2  35923  isnumbasgrplem3  35964  proot1mul  36073  stoweidlem11  37871  stoweidlem14  37874  afv0nbfvbi  38653