Theorem sylan2i 465

Description: A syllogism inference.

Hypotheses

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

Assertion

Ref	Expression
sylan2i	|- (ph -> ((ps /\ ta) -> th))

Proof of Theorem sylan2i

Step	Hyp	Ref	Expression
1		sylan2i.1	. 2 |- (ph -> ((ps /\ ch) -> th))
2		sylan2i.2	. . 3 |- (ta -> ch)
3	2	a1i 8	. 2 |- (ph -> (ta -> ch))
4	1, 3	sylan2d 458	1 |- (ph -> ((ps /\ ta) -> th))

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  syl2ani 466  odi 4203  sdomentr 4459  sdomtr 4463  pssnn 4522  noinfep 4623  rankr1 4657  ltaddpr 5123  ltexprlem7 5131  ltaprlem 5133  prlem936b 5137  reclem3pr 5141  divdivdivt 5751  sup2 6008  lmcau 7958  spanunsn 9459  pjnormss 10052

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