Metamath Proof Explorer


Theorem pm5.53

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

Ref Expression
Assertion pm5.53 φψχθφθψθχθ

Proof

Step Hyp Ref Expression
1 jaob φψχθφψθχθ
2 jaob φψθφθψθ
3 2 anbi1i φψθχθφθψθχθ
4 1 3 bitri φψχθφθψθχθ