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  5923  fcof1o  5930  isoselem  5961  isose  5962  tposss  6412  smoiso  6468  fzssp1  10302  fzosplitsnm1  10455  fzofzp1  10473  fzostep1  10484  bcm1k  11023  pfxccatpfx2  11322  climuni  11871  serf0  11930  fsumparts  12049  hashiun  12057  oddprm  12850  znzrh2  14679  znf1o  14684  znidom  14690  hmeores  15058  gausslemma2dlem0c  15799  gausslemma2dlem0e  15801  gausslemma2dlem1a  15806  eupthvdres  16345