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 3746  funfv 3761  fvopab2 3782  omword 4191  oeword 4207  th3qlem1 4304  axrnegex 5263  mulc1cncf 7222  effsumle 7346  neindisj 7681  pilem2 8610  logeftb 8703  unopbdt 9878  nmcoplbt 9898  nmcfnlbt 9927  nmopco 9966

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