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 3896  odi 4210  divadddivt 5784  fsumsplit 7020  iserzcmp0 7143  cvgratlem1 7250  infpnlem1 7506  lpbl 7880  lmsslem 7952  lmle 7960  cmsss 7997  bcthlem1 7999  sspph 8515  unoplint 9844  hmoplint 9866  irredlem1 10317  mdsymlem2 10331

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