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 4156  oelim 4159  cnegextlem3 5327  mulsubt 5457  divadddivt 5748  divexpt 6538  isum1p 7149  infxpidmlem12 7514  metcnp 7839  lmle 7911  xpcn 7926  bcthlem27 7975  cnlnadjlem2 9939  irredlem2 10255  mdsymlem5 10271

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