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  5825  fcof1o  5832  isoselem  5863  isose  5864  tposss  6299  smoiso  6355  fzssp1  10133  fzosplitsnm1  10276  fzofzp1  10294  fzostep1  10304  bcm1k  10831  climuni  11436  serf0  11495  fsumparts  11613  hashiun  11621  oddprm  12397  znzrh2  14134  znf1o  14139  znidom  14145  hmeores  14483  gausslemma2dlem0c  15167  gausslemma2dlem0e  15169  gausslemma2dlem1a  15174