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  5918  fcof1o  5925  isoselem  5956  isose  5957  tposss  6407  smoiso  6463  fzssp1  10292  fzosplitsnm1  10444  fzofzp1  10462  fzostep1  10473  bcm1k  11012  pfxccatpfx2  11308  climuni  11844  serf0  11903  fsumparts  12021  hashiun  12029  oddprm  12822  znzrh2  14650  znf1o  14655  znidom  14661  hmeores  15029  gausslemma2dlem0c  15770  gausslemma2dlem0e  15772  gausslemma2dlem1a  15777