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 )

This proof depends on syntax axioms:   -> wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  f1ocnvfvrneq  5991  fcof1o  5998  isoselem  6029  isose  6030  tposss  6522  smoiso  6578  fzssp1  10489  fzosplitsnm1  10643  fzofzp1  10661  fzostep1  10672  bcm1k  11219  pfxccatpfx2  11530  climuni  12083  serf0  12142  fsumparts  12261  hashiun  12269  oddprm  13066  znzrh2  15089  znf1o  15094  znidom  15100  hmeores  15558  ppinprm  16277  chtnprm  16279  gausslemma2dlem0c  16392  gausslemma2dlem0e  16394  gausslemma2dlem1a  16399  eupthvdres  16938