Metamath Proof Explorer


Theorem bitr

Description: Theorem *4.22 of WhiteheadRussell p. 117. bitri in closed form. (Contributed by NM, 3-Jan-2005)

Ref Expression
Assertion bitr φ ψ ψ χ φ χ

Proof

Step Hyp Ref Expression
1 bibi1 φ ψ φ χ ψ χ
2 1 biimpar φ ψ ψ χ φ χ