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  5906  fcof1o  5913  isoselem  5944  isose  5945  tposss  6392  smoiso  6448  fzssp1  10263  fzosplitsnm1  10415  fzofzp1  10433  fzostep1  10443  bcm1k  10982  pfxccatpfx2  11269  climuni  11804  serf0  11863  fsumparts  11981  hashiun  11989  oddprm  12782  znzrh2  14610  znf1o  14615  znidom  14621  hmeores  14989  gausslemma2dlem0c  15730  gausslemma2dlem0e  15732  gausslemma2dlem1a  15737