Metamath Proof Explorer


Theorem bitr2di

Description: A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993)

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

Proof

Step Hyp Ref Expression
1 bitr2di.1 φ ψ χ
2 bitr2di.2 χ θ
3 1 2 bitrdi φ ψ θ
4 3 bicomd φ θ ψ