This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sylbi

Description: A mixed syllogism inference from a biconditional and an implication. Useful for substituting an antecedent with a definition. (Contributed by NM, 3-Jan-1993)

Ref Expression
Hypotheses sylbi.1 
|- ( ph <-> ps )
sylbi.2 
|- ( ps -> ch )
Assertion sylbi 
|- ( ph -> ch )

Proof

Step Hyp Ref Expression
1 sylbi.1 
 |-  ( ph <-> ps )
2 sylbi.2 
 |-  ( ps -> ch )
3 1 biimpi 
 |-  ( ph -> ps )
4 3 2 syl 
 |-  ( ph -> ch )