Metamath Proof Explorer


Theorem syl6rbbr

Description: A syllogism inference from two biconditionals. (Contributed by NM, 25-Nov-1994)

Ref Expression
Hypotheses syl6rbbr.1 φ ψ χ
syl6rbbr.2 θ χ
Assertion syl6rbbr φ θ ψ

Proof

Step Hyp Ref Expression
1 syl6rbbr.1 φ ψ χ
2 syl6rbbr.2 θ χ
3 2 bicomi χ θ
4 1 3 syl6rbb φ θ ψ