Theorem 4syl 21

Description: Inference chaining three syllogisms. (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  1886  aevlem1OLD  2033  eqeq1d  2469  2reu5  3312  f1ocnvfvrneq  6175  isoselem  6223  isose  6225  fnwelem  6895  tposss  6953  smoiso  7030  nneob  7298  difsnen  7596  ordtypelem10  7948  oismo  7961  cantnflt2  8088  oemapso  8097  cantnf  8108  cantnfclOLD  8112  cantnflt2OLD  8118  cantnfOLD  8130  mapfienOLD  8134  scott0  8300  tskwe  8327  infxpenlem  8387  ac10ct  8411  acndom  8428  dfac12lem2  8520  dfac12r  8522  pwcdadom  8592  ackbij1lem15  8610  ackbij2lem2  8616  ackbij2lem3  8617  ackbij2  8619  fin23lem22  8703  domtriomlem  8818  axdc3lem2  8827  sdomsdomcard  8931  canthp1lem2  9027  pwfseqlem5  9037  gchhar  9053  fzssp1  11722  fzosplitsnm1  11854  fzofzp1  11873  fzostep1  11886  bcm1k  12357  swrdccat2  12642  revccat  12699  revrev  12700  climuni  13334  isercolllem2  13447  isercoll  13449  serf0  13462  fsumparts  13579  hashiun  13595  isumsup2  13617  climcndslem1  13620  climcndslem2  13621  oddprm  14194  vdwmc  14351  prdsplusg  14709  prdsvsca  14711  imasdsval2  14767  sscpwex  15041  ssc2  15048  pmtrfv  16273  symgtrinv  16293  odcl2  16383  lsmmod  16489  efgsdmi  16546  gsumval3OLD  16699  gsumzinv  16760  gsumzinvOLD  16761  ablfac1b  16911  pgpfac1lem1  16915  pgpfaclem2  16923  ablfaclem2  16927  ablfac  16929  srng0  17292  mpfsubrg  17972  pf1subrg  18155  mpfpf1  18158  pf1mpf  18159  znzrh2  18351  znf1o  18357  znhash  18364  znfld  18366  cygznlem3  18375  ip2di  18443  iscncl  19536  qtopcmap  19955  hmeores  20007  qtopf1  20052  fbssfi  20073  filssufil  20148  fmfnfmlem3  20192  clssubg  20342  tmsxms  20724  prdsxms  20768  metustfbas  20804  metuel2  20817  restmetu  20825  nrginvrcn  20935  nmhmcn  21338  iscmet3  21467  minveclem3  21579  ovoliunlem2  21649  ismbf3d  21796  i1fd  21823  dvadd  22078  dvmul  22079  dvaddf  22080  dvco  22085  dvcof  22086  dvcnvlem  22112  mdeglt  22200  dgrub  22366  plyremlem  22434  fta1lem  22437  fta1  22438  vieta1lem2  22441  plyexmo  22443  elaa  22446  ulmcau  22524  ulmdvlem3  22531  ppinprm  23154  chtnprm  23156  dchrzrh1  23247  dchr1  23260  dchr1re  23266  dchrptlem1  23267  dchrpt  23270  dchrsum2  23271  dchrhash  23274  rpvmasumlem  23400  rpvmasum2  23425  mudivsum  23443  f1otrg  23850  cyclnspth  24307  el2spthonot  24546  usgravd0nedg  24594  subgores  24982  rngosn  25082  minvecolem3  25468  orngmullt  27462  pl1cn  27573  zrhunitpreima  27595  qqhnm  27607  qqhucn  27609  ddemeas  27848  1stmbfm  27871  2ndmbfm  27872  omsval  27904  unveldomd  27994  probmeasb  28009  signstfvp  28168  signstres  28172  subfacp1lem5  28268  erdsze2lem1  28287  cvmseu  28361  cvmliftlem11  28380  cvmlift3lem8  28411  cvmlift3lem9  28412  ghomfo  28506  relexpsucr  28528  binomfallfaclem2  28739  wfrlem5  28924  frrlem5  28968  meran1  29453  lukshef-ax2  29457  ordcmp  29489  wl-nfeqfb  29567  mblfinlem2  29629  trer  29711  sdclem2  29838  ismtyhmeolem  29903  heiborlem10  29919  aomclem6  30609  kelac1  30613  kelac2  30615  isnumbasgrplem3  30658  proot1mul  30761  stoweidlem11  31311  stoweidlem14  31314  afv0nbfvbi  31703  bnj1098  32921  bj-aevlem1v  33401  lpssat  33810  lssatle  33812  lssat  33813  cdlemk45  35743  dia2dimlem9  35869  diblsmopel  35968  dochspss  36175  baerlem5blem2  36509  hdmap14lem4a  36671