Metamath Proof Explorer


Theorem sylbb1

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

Ref Expression
Hypotheses sylbb1.1 φ ψ
sylbb1.2 φ χ
Assertion sylbb1 ψ χ

Proof

Step Hyp Ref Expression
1 sylbb1.1 φ ψ
2 sylbb1.2 φ χ
3 1 biimpri ψ φ
4 3 2 sylib ψ χ