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  5978  fcof1o  5985  isoselem  6016  isose  6017  tposss  6507  smoiso  6563  fzssp1  10451  fzosplitsnm1  10605  fzofzp1  10623  fzostep1  10634  bcm1k  11176  pfxccatpfx2  11487  climuni  12037  serf0  12096  fsumparts  12215  hashiun  12223  oddprm  13016  znzrh2  14953  znf1o  14958  znidom  14964  hmeores  15339  gausslemma2dlem0c  16084  gausslemma2dlem0e  16086  gausslemma2dlem1a  16091  eupthvdres  16630