Metamath Proof Explorer


Theorem pm4.45

Description: Theorem *4.45 of WhiteheadRussell p. 119. (Contributed by NM, 3-Jan-2005)

Ref Expression
Assertion pm4.45 φφφψ

Proof

Step Hyp Ref Expression
1 orc φφψ
2 1 pm4.71i φφφψ