Theorem 4syl 21

Description: Inference chaining three syllogisms syl 16. (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 20	. 2 |- ( ph -> th )
5		4syl.4	. 2 |- ( th -> ta )
6	4, 5	syl 16	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  1925  aevlem1OLD  2046  eqeq1d  2445  2reu5  3294  f1ocnvfvrneq  6174  isoselem  6222  isose  6224  fnwelem  6900  tposss  6958  smoiso  7035  nneob  7303  difsnen  7601  ordtypelem10  7955  oismo  7968  cantnflt2  8095  oemapso  8104  cantnf  8115  cantnfclOLD  8119  cantnflt2OLD  8125  cantnfOLD  8137  mapfienOLD  8141  scott0  8307  tskwe  8334  infxpenlem  8394  ac10ct  8418  acndom  8435  dfac12lem2  8527  dfac12r  8529  pwcdadom  8599  ackbij1lem15  8617  ackbij2lem2  8623  ackbij2lem3  8624  ackbij2  8626  fin23lem22  8710  domtriomlem  8825  axdc3lem2  8834  sdomsdomcard  8938  canthp1lem2  9034  pwfseqlem5  9044  gchhar  9060  fzssp1  11737  fzosplitsnm1  11872  fzofzp1  11891  fzostep1  11904  bcm1k  12375  swrdccat2  12665  revccat  12722  revrev  12723  climuni  13357  isercolllem2  13470  isercoll  13472  serf0  13485  fsumparts  13602  hashiun  13618  isumsup2  13640  climcndslem1  13643  climcndslem2  13644  oddprm  14321  vdwmc  14478  prdsplusg  14837  prdsvsca  14839  imasdsval2  14895  sscpwex  15166  ssc2  15173  pmtrfv  16456  symgtrinv  16476  odcl2  16566  lsmmod  16672  efgsdmi  16729  gsumval3OLD  16887  gsumzinv  16948  gsumzinvOLD  16949  ablfac1b  17100  pgpfac1lem1  17104  pgpfaclem2  17112  ablfaclem2  17116  ablfac  17118  srng0  17488  mpfsubrg  18180  pf1subrg  18363  mpfpf1  18366  pf1mpf  18367  znzrh2  18562  znf1o  18568  znhash  18575  znfld  18577  cygznlem3  18586  ip2di  18654  iscncl  19748  qtopcmap  20198  hmeores  20250  qtopf1  20295  fbssfi  20316  filssufil  20391  fmfnfmlem3  20435  clssubg  20585  tmsxms  20967  prdsxms  21011  metustfbas  21047  metuel2  21060  restmetu  21068  nrginvrcn  21178  nmhmcn  21581  iscmet3  21710  minveclem3  21822  ovoliunlem2  21892  ismbf3d  22039  i1fd  22066  dvadd  22321  dvmul  22322  dvaddf  22323  dvco  22328  dvcof  22329  dvcnvlem  22355  mdeglt  22443  dgrub  22609  plyremlem  22678  fta1lem  22681  fta1  22682  vieta1lem2  22685  plyexmo  22687  elaa  22690  ulmcau  22768  ulmdvlem3  22775  ppinprm  23404  chtnprm  23406  dchrzrh1  23497  dchr1  23510  dchr1re  23516  dchrptlem1  23517  dchrpt  23520  dchrsum2  23521  dchrhash  23524  rpvmasumlem  23650  rpvmasum2  23675  mudivsum  23693  f1otrg  24152  cyclnspth  24609  el2spthonot  24848  usgravd0nedg  24896  subgores  25284  rngosn  25384  minvecolem3  25770  orngmullt  27777  locfinref  27822  pl1cn  27915  zrhunitpreima  27937  qqhnm  27949  qqhucn  27951  ddemeas  28186  1stmbfm  28209  2ndmbfm  28210  omsval  28242  unveldomd  28332  probmeasb  28347  signstfvp  28506  signstres  28510  subfacp1lem5  28606  erdsze2lem1  28625  cvmseu  28699  cvmliftlem11  28718  cvmlift3lem8  28749  cvmlift3lem9  28750  ghomfo  29009  relexpsucr  29031  binomfallfaclem2  29138  wfrlem5  29323  frrlem5  29367  meran1  29852  lukshef-ax2  29856  ordcmp  29888  wl-nfeqfb  29966  mblfinlem2  30028  trer  30110  sdclem2  30211  ismtyhmeolem  30276  heiborlem10  30292  aomclem6  30981  kelac1  30985  kelac2  30987  isnumbasgrplem3  31030  proot1mul  31132  stoweidlem11  31747  stoweidlem14  31750  afv0nbfvbi  32190  bnj1098  33710  bj-aevlem1v  34203  lpssat  34613  lssatle  34615  lssat  34616  cdlemk45  36548  dia2dimlem9  36674  diblsmopel  36773  dochspss  36980  baerlem5blem2  37314  hdmap14lem4a  37476