Theorem sylan2i 357

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 7	. 2 |- (ph -> (ta -> ch))
4	1, 3	sylan2d 353	1 |- (ph -> ((ps /\ ta ) -> th))

Syntax hints:   -> wi 2   /\ wa 196

This theorem is referenced by:  syl2ani 358  sdomentr 3371  sdomtr 3373  pssnn 3428  rankr1 3518  ltaddpr 3934  ltexprlem7 3942  ltaprlem 3944  prlem936b 3948  reclem3pr 3952  divdivdivt 4265  sup2 4510  spanunsn 5482  pjnormss 5638

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org