Database
CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY
Propositional calculus
Logical "nand" (Sheffer stroke)
nanan
Next ⟩
dfnan2
Metamath Proof Explorer
Ascii
Unicode
Theorem
nanan
Description:
Conjunction in terms of alternative denial.
(Contributed by
Mario Carneiro
, 9-May-2015)
Ref
Expression
Assertion
nanan
⊢
φ
∧
ψ
↔
¬
φ
⊼
ψ
Proof
Step
Hyp
Ref
Expression
1
df-nan
⊢
φ
⊼
ψ
↔
¬
φ
∧
ψ
2
1
con2bii
⊢
φ
∧
ψ
↔
¬
φ
⊼
ψ