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  5922  fcof1o  5929  isoselem  5960  isose  5961  tposss  6411  smoiso  6467  fzssp1  10301  fzosplitsnm1  10453  fzofzp1  10471  fzostep1  10482  bcm1k  11021  pfxccatpfx2  11317  climuni  11853  serf0  11912  fsumparts  12030  hashiun  12038  oddprm  12831  znzrh2  14659  znf1o  14664  znidom  14670  hmeores  15038  gausslemma2dlem0c  15779  gausslemma2dlem0e  15781  gausslemma2dlem1a  15786