Metamath Proof Explorer

Theorem nornot

Description: -. is expressible via -\/ . (Contributed by Remi, 25-Oct-2023) (Proof shortened by Wolf Lammen, 8-Dec-2023)

Ref Expression
Assertion nornot 
|- ( -. ph <-> ( ph -\/ ph ) )

Proof

Step Hyp Ref Expression
1 df-nor 
 |-  ( ( ph -\/ ph ) <-> -. ( ph \/ ph ) )
2 oridm 
 |-  ( ( ph \/ ph ) <-> ph )
3 1 2 xchbinx 
 |-  ( ( ph -\/ ph ) <-> -. ph )
4 3 bicomi 
 |-  ( -. ph <-> ( ph -\/ ph ) )