Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Richard Penner
Propositions from _Begriffsschrift_
_Begriffsschrift_ Chapter II Implication and Negation
axfrege41
Next ⟩
ax-frege41
Metamath Proof Explorer
Ascii
Unicode
Theorem
axfrege41
Description:
Identical to
notnot
. Axiom 41 of
Frege1879
p. 47.
(Contributed by
RP
, 24-Dec-2019)
Ref
Expression
Assertion
axfrege41
⊢
φ
→
¬
¬
φ
Proof
Step
Hyp
Ref
Expression
1
notnot
⊢
φ
→
¬
¬
φ