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  5874  fcof1o  5881  isoselem  5912  isose  5913  tposss  6355  smoiso  6411  fzssp1  10224  fzosplitsnm1  10375  fzofzp1  10393  fzostep1  10403  bcm1k  10942  pfxccatpfx2  11228  climuni  11719  serf0  11778  fsumparts  11896  hashiun  11904  oddprm  12697  znzrh2  14523  znf1o  14528  znidom  14534  hmeores  14902  gausslemma2dlem0c  15643  gausslemma2dlem0e  15645  gausslemma2dlem1a  15650