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 4210  sdomentr 4470  sdomtr 4474  pssnn 4534  noinfep 4640  rankr1 4674  ltaddpr 5140  ltexprlem7 5148  ltaprlem 5150  prlem936b 5154  reclem3pr 5158  divdivdivt 5785  sup2 6051  lmcau 7996  spanunsn 9502  pjnormss 10096

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