Theorem 4syl 18

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. (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 17	. 2 |- ( ph -> th )
5		4syl.4	. 2 |- ( th -> ta )
6	4, 5	syl 14	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:  f1ocnvfvrneq  5955  fcof1o  5962  isoselem  5993  isose  5994  tposss  6477  smoiso  6533  fzssp1  10401  fzosplitsnm1  10554  fzofzp1  10572  fzostep1  10583  bcm1k  11122  pfxccatpfx2  11429  climuni  11978  serf0  12037  fsumparts  12156  hashiun  12164  oddprm  12957  znzrh2  14794  znf1o  14799  znidom  14805  hmeores  15180  gausslemma2dlem0c  15924  gausslemma2dlem0e  15926  gausslemma2dlem1a  15931  eupthvdres  16470