Metamath Proof Explorer

Theorem sylbb2

Description: A mixed syllogism inference from two biconditionals. (Contributed by BJ, 21-Apr-2019)

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

Proof

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