Theorem 4syl 21

Description: Inference chaining three syllogisms. 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. (Contributed by BJ, 14-Jul-2018.) (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  2012  2reu5  3164  f1ocnvfvrneq  5987  fcof1o  5994  isoselem  6029  isose  6031  fnwelem  6686  tposss  6745  smoiso  6819  nneob  7087  difsnen  7389  ordtypelem10  7737  oismo  7750  cantnflt2  7877  oemapso  7886  cantnf  7897  cantnfclOLD  7901  cantnflt2OLD  7907  cantnfOLD  7919  mapfienOLD  7923  scott0  8089  tskwe  8116  infxpenlem  8176  ac10ct  8200  acndom  8217  dfac12lem2  8309  dfac12r  8311  pwcdadom  8381  ackbij1lem15  8399  ackbij2lem2  8405  ackbij2lem3  8406  ackbij2  8408  fin23lem22  8492  domtriomlem  8607  axdc3lem2  8616  sdomsdomcard  8720  canthp1lem2  8816  pwfseqlem5  8826  gchhar  8842  fzssp1  11497  fzosplitsnm1  11604  fzofzp1  11620  fzostep1  11631  bcm1k  12087  swrdccat2  12348  revccat  12402  revrev  12403  climuni  13026  isercolllem2  13139  isercoll  13141  serf0  13154  fsumparts  13265  hashiun  13281  isumsup2  13305  climcndslem1  13308  climcndslem2  13309  oddprm  13878  vdwmc  14035  prdsplusg  14392  prdsvsca  14394  imasdsval2  14450  sscpwex  14724  ssc2  14731  pmtrfv  15951  symgtrinv  15971  odcl2  16059  lsmmod  16165  efgsdmi  16222  gsumval3OLD  16375  gsumzinv  16434  gsumzinvOLD  16435  ablfac1b  16561  pgpfac1lem1  16565  pgpfaclem2  16573  ablfaclem2  16577  ablfac  16579  srng0  16925  mpfsubrg  17594  pf1subrg  17751  mpfpf1  17754  pf1mpf  17755  znzrh2  17937  znf1o  17943  znhash  17950  znfld  17952  cygznlem3  17961  ip2di  18029  iscncl  18832  qtopcmap  19251  hmeores  19303  qtopf1  19348  fbssfi  19369  filssufil  19444  fmfnfmlem3  19488  clssubg  19638  tmsxms  20020  prdsxms  20064  metustfbas  20100  metuel2  20113  restmetu  20121  nrginvrcn  20231  nmhmcn  20634  iscmet3  20763  minveclem3  20875  ovoliunlem2  20945  ismbf3d  21091  i1fd  21118  dvadd  21373  dvmul  21374  dvaddf  21375  dvco  21380  dvcof  21381  dvcnvlem  21407  mdeglt  21495  dgrub  21661  plyremlem  21729  fta1lem  21732  fta1  21733  vieta1lem2  21736  plyexmo  21738  elaa  21741  ulmcau  21819  ulmdvlem3  21826  ppinprm  22449  chtnprm  22451  dchrzrh1  22542  dchr1  22555  dchr1re  22561  dchrptlem1  22562  dchrpt  22565  dchrsum2  22566  dchrhash  22569  rpvmasumlem  22695  rpvmasum2  22720  mudivsum  22738  f1otrg  23052  cyclnspth  23452  usgravd0nedg  23517  subgores  23726  rngosn  23826  minvecolem3  24212  orngmullt  26212  pl1cn  26321  zrhunitpreima  26343  qqhnm  26355  qqhucn  26357  ddemeas  26588  1stmbfm  26611  2ndmbfm  26612  unveldomd  26728  probmeasb  26743  signstfvp  26902  signstres  26906  subfacp1lem5  27002  erdsze2lem1  27021  cvmseu  27095  cvmliftlem11  27114  cvmlift3lem8  27145  cvmlift3lem9  27146  ghomfo  27239  relexpsucr  27261  binomfallfaclem2  27472  wfrlem5  27657  frrlem5  27701  meran1  28187  lukshef-ax2  28191  ordcmp  28223  wl-nfeqfb  28295  mblfinlem2  28354  trer  28436  sdclem2  28563  ismtyhmeolem  28628  heiborlem10  28644  aomclem6  29337  kelac1  29341  kelac2  29343  isnumbasgrplem3  29386  proot1mul  29489  stoweidlem11  29731  stoweidlem14  29734  afv0nbfvbi  29982  el2spthonot  30314  bnj1098  31611  bj-aevlem1v  32018  lpssat  32380  lssatle  32382  lssat  32383  cdlemk45  34313  dia2dimlem9  34439  diblsmopel  34538  dochspss  34745  baerlem5blem2  35079  hdmap14lem4a  35241