Theorem sylanl1 460

Description: A syllogism inference.

Hypotheses

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

Assertion

Ref	Expression
sylanl1	|- (((ta /\ ps) /\ ch) -> th)

Proof of Theorem sylanl1

Step	Hyp	Ref	Expression
1		sylanl1.1	. 2 |- (((ph /\ ps) /\ ch) -> th)
2		sylanl1.2	. . 3 |- (ta -> ph)
3	2	anim1i 334	. 2 |- ((ta /\ ps) -> (ph /\ ps))
4	1, 3	sylan 448	1 |- (((ta /\ ps) /\ ch) -> th)

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  isocnv 3881  odi 4194  divadddivt 5740  fsumsplit 6958  iserzcmp0 7079  cvgratlem1 7185  infpnlem1 7449  lpbl 7819  lmsslem 7887  lmle 7895  cmsss 7931  bcthlem1 7933  sspph 8446  unoplint 9760  hmoplint 9782  irredlem1 10225  mdsymlem2 10239

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