Theorem syl7 23

Description: A syllogism rule of inference. The second premise is used to replace the third antecedent of the first premise.

Hypotheses

Ref	Expression
syl7.1	|- (ph -> (ps -> (ch -> th)))
syl7.2	|- (ta -> ch)

Assertion

Ref	Expression
syl7	|- (ph -> (ps -> (ta -> th)))

Proof of Theorem syl7

Step	Hyp	Ref	Expression
1		syl7.1	. 2 |- (ph -> (ps -> (ch -> th)))
2		syl7.2	. . 3 |- (ta -> ch)
3	2	imim1i 16	. 2 |- ((ch -> th) -> (ta -> th))
4	1, 3	syl6 22	1 |- (ph -> (ps -> (ta -> th)))

Syntax hints:   -> wi 3

This theorem is referenced by:  syl7ib 216  syl3an3 863  hbae 1147  ax11 1221  a12study 1380  uniiunlem 2135  tz7.7 2979  f1oweALT 3912  nneneq 4518  r1ord 4665  ltbtwnpq 5096  nnunb 6072  iscms2lem5 7990  atcvat4 10319  mdsymlem5 10329  sumdmdi 10337  unpde2eg2 10530  icmpmon 10715

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-mp 7

Copyright terms: Public domain