Theorem sylanbr 450

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	biimpr 152	. 2 |- (th -> ph)
4	1, 3	sylan 448	1 |- ((th /\ ps) -> ch)

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223

This theorem is referenced by:  syl2anbr 456  funbrfvb 3755  funfv 3770  fvopab2 3791  omword 4201  oeword 4217  th3qlem1 4314  axrnegex 5283  mulc1cncf 7279  effsumle 7397  neindisj 7731  pilem2 8672  logeftb 8764  unopbdt 9940  nmcoplbt 9960  nmcfnlbt 9989  nmopco 10028

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