Theorem sylanbr 452

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 450	1 |- ((th /\ ps) -> ch)

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

This theorem is referenced by:  syl2anbr 458  funbrfvb 3761  funfv 3776  fvopab2 3797  omword 4207  oeword 4223  th3qlem1 4320  axrnegex 5295  mulc1cncf 7279  effsumle 7397  neindisj 7728  pilem2 8667  logeftb 8759  unopbdt 9935  nmcoplbt 9955  nmcfnlbt 9984  nmopco 10023

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