HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
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
StepHypRef Expression
1 sylan.1 . 2 |- ((ph /\ ps) -> ch)
2 sylanbr.2 . . 3 |- (ph <-> th)
32biimpr 152 . 2 |- (th -> ph)
41, 3sylan 448 1 |- ((th /\ ps) -> ch)
Colors of variables: wff set class
Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223
This theorem is referenced by:  syl2anbr 456  funbrfvb 3740  funfv 3755  fvopab2 3776  omword 4185  oeword 4201  th3qlem1 4298  axrnegex 5255  mulc1cncf 7214  effsumle 7338  neindisj 7672  pilem2 8591  logeftb 8686  unopbdt 9855  nmcoplbt 9875  nmcfnlbt 9904  nmopco 9942
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