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 φψψχφχ