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  5829  fcof1o  5836  isoselem  5867  isose  5868  tposss  6304  smoiso  6360  fzssp1  10142  fzosplitsnm1  10285  fzofzp1  10303  fzostep1  10313  bcm1k  10852  climuni  11458  serf0  11517  fsumparts  11635  hashiun  11643  oddprm  12428  znzrh2  14202  znf1o  14207  znidom  14213  hmeores  14551  gausslemma2dlem0c  15292  gausslemma2dlem0e  15294  gausslemma2dlem1a  15299