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