Theorem sylanbr 499

Description: A syllogism inference.

Hypotheses

Ref	Expression
sylan.1	|- ((ph /\ ps) -> ch)
sylanbr.2	|- (ph <-> th)

Assertion

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

Proof of Theorem sylanbr

Step	Hyp	Ref	Expression
1		sylan.1	. 2 |- ((ph /\ ps) -> ch)
2		sylanbr.2	. . 3 |- (ph <-> th)
3	2	biimpri 169	. 2 |- (th -> ph)
4	1, 3	sylan 497	1 |- ((th /\ ps) -> ch)

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240

This theorem is referenced by:  syl2anbr 505  funbrfvb 4714  funfv 4731  fvopab2 4754  omword 5249  oeword 5265  th3qlem1 5373  axrnegex 6436  mulc1cncf 8541  effsumlei 8662  neindisj 9007  pilem2 10021  logeftb 10118  unopbd 11577  nmcoplb 11597  nmcfnlb 11626  nmopcoi 11665  fseq1cl 13619  isprm2lem 13774

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