Metamath Proof Explorer

Theorem sylbb1

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

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

Proof

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