Metamath Proof Explorer


Theorem pm3.48

Description: Theorem *3.48 of WhiteheadRussell p. 114. (Contributed by NM, 28-Jan-1997)

Ref Expression
Assertion pm3.48 φψχθφχψθ

Proof

Step Hyp Ref Expression
1 orc ψψθ
2 1 imim2i φψφψθ
3 olc θψθ
4 3 imim2i χθχψθ
5 2 4 jaao φψχθφχψθ