Theorem sylan2i 514

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 507	1 |- (ph -> ((ps /\ ta) -> th))

Syntax hints:   -> wi 3   /\ wa 240

This theorem is referenced by:  syl2ani 515  odi 5258  sdomentr 5533  sdomtr 5537  pssnn 5628  noinfep 5747  rankr1 5785  ltaddpr 6292  ltexprlem7 6300  ltaprlem 6302  prlem936b 6306  reclem3pr 6310  sup2 7260  lmcau 9274  fbunfip 10282  spanunsni 11135  pjnormssi 11740  filufint 15574

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 164  df-an 242

Copyright terms: Public domain