Metamath Proof Explorer


Theorem bitr3di

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

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

Proof

Step Hyp Ref Expression
1 bitr3di.1 φψχ
2 bitr3di.2 ψθ
3 2 bicomi θψ
4 3 1 bitr2id φχθ