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 4150  oelim 4153  cnegextlem3 5319  mulsubt 5449  divadddivt 5740  divexpt 6530  isum1p 7141  infxpidmlem12 7506  metcnp 7826  lmle 7895  xpcn 7910  bcthlem27 7959  cnlnadjlem2 9916  irredlem2 10226  mdsymlem5 10242

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