Theorem sylanl1 509

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

Syntax hints:   -> wi 3   /\ wa 240

This theorem is referenced by:  isocnv 4873  odi 5258  oeoelem 5273  fsumsplit 8280  iserzcmp0 8403  cvgratlem1 8512  infpnlem1 8775  lpbl 9157  lmsslem 9230  lmle 9238  cmsss 9275  bcthlem1 9277  ssga 9455  sspph 9856  unoplin 11481  hmoplin 11503  irredlem1 11962  mdsymlem2 11976  eucalginv 13752  foco2 15686  sdc 15811  cnres 15889  rrntotbnd 16022  isfldidl 16216  ispridlc 16218  pointpsub 17231

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