Metamath Proof Explorer

Theorem pm4.52

Description: Theorem *4.52 of WhiteheadRussell p. 120. (Contributed by NM, 3-Jan-2005) (Proof shortened by Wolf Lammen, 5-Nov-2012)

Ref Expression
Assertion pm4.52 
|- ( ( ph /\ -. ps ) <-> -. ( -. ph \/ ps ) )

Proof

Step Hyp Ref Expression
1 annim 
 |-  ( ( ph /\ -. ps ) <-> -. ( ph -> ps ) )
2 imor 
 |-  ( ( ph -> ps ) <-> ( -. ph \/ ps ) )
3 1 2 xchbinx 
 |-  ( ( ph /\ -. ps ) <-> -. ( -. ph \/ ps ) )