Theorem sylanl2 461

Description: A syllogism inference.

Hypotheses

Ref	Expression
sylanl2.1	|- (((ph /\ ps) /\ ch) -> th)
sylanl2.2	|- (ta -> ps)

Assertion

Ref	Expression
sylanl2	|- (((ph /\ ta) /\ ch) -> th)

Proof of Theorem sylanl2

Step	Hyp	Ref	Expression
1		sylanl2.1	. 2 |- (((ph /\ ps) /\ ch) -> th)
2		sylanl2.2	. . 3 |- (ta -> ps)
3	2	anim2i 335	. 2 |- ((ph /\ ta) -> (ph /\ ps))
4	1, 3	sylan 448	1 |- (((ph /\ ta) /\ ch) -> th)

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  oesuc 4166  oelim 4169  cnegextlem3 5347  mulsubt 5477  divadddivt 5784  divexpt 6599  isum1p 7206  infxpidmlem12 7563  metcnp 7887  lmle 7960  xpcn 7976  bcthlem27 8025  cnlnadjlem2 10001  irredlem2 10318  mdsymlem5 10334

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

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain