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  5912  fcof1o  5919  isoselem  5950  isose  5951  tposss  6398  smoiso  6454  fzssp1  10275  fzosplitsnm1  10427  fzofzp1  10445  fzostep1  10455  bcm1k  10994  pfxccatpfx2  11285  climuni  11820  serf0  11879  fsumparts  11997  hashiun  12005  oddprm  12798  znzrh2  14626  znf1o  14631  znidom  14637  hmeores  15005  gausslemma2dlem0c  15746  gausslemma2dlem0e  15748  gausslemma2dlem1a  15753