Metamath Proof Explorer

Theorem pm5.19

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

Ref Expression
Assertion pm5.19 
|- -. ( ph <-> -. ph )

Proof

Step Hyp Ref Expression
1 biid 
 |-  ( ph <-> ph )
2 pm5.18 
 |-  ( ( ph <-> ph ) <-> -. ( ph <-> -. ph ) )
3 1 2 mpbi 
 |-  -. ( ph <-> -. ph )