Metamath Proof Explorer

Axiom ax-frege31

Description: ph cannot be denied and (at the same time ) -. -. ph affirmed. Duplex negatio affirmat. The denial of the denial is affirmation. Identical to notnotr . Axiom 31 of Frege1879 p. 44. (Contributed by RP, 24-Dec-2019) (New usage is discouraged.)

Ref Expression
Assertion ax-frege31 
|- ( -. -. ph -> ph )

Detailed syntax breakdown

Step Hyp Ref Expression
0 wph 
 |-  ph
1 0 wn 
 |-  -. ph
2 1 wn 
 |-  -. -. ph
3 2 0 wi 
 |-  ( -. -. ph -> ph )