Metamath Proof Explorer


Theorem bitr2d

Description: Deduction form of bitr2i . (Contributed by NM, 9-Jun-2004)

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

Proof

Step Hyp Ref Expression
1 bitr2d.1 φψχ
2 bitr2d.2 φχθ
3 1 2 bitrd φψθ
4 3 bicomd φθψ