Database
CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY
Propositional calculus
Logical "nand" (Sheffer stroke)
nanim
Next ⟩
nannot
Metamath Proof Explorer
Ascii
Unicode
Theorem
nanim
Description:
Implication in terms of alternative denial.
(Contributed by
Jeff Hoffman
, 19-Nov-2007)
Ref
Expression
Assertion
nanim
⊢
φ
→
ψ
↔
φ
⊼
ψ
⊼
ψ
Proof
Step
Hyp
Ref
Expression
1
nannan
⊢
φ
⊼
ψ
⊼
ψ
↔
φ
→
ψ
∧
ψ
2
anidmdbi
⊢
φ
→
ψ
∧
ψ
↔
φ
→
ψ
3
1
2
bitr2i
⊢
φ
→
ψ
↔
φ
⊼
ψ
⊼
ψ