Metamath Proof Explorer

Theorem nic-dfim

Description: This theorem "defines" implication in terms of 'nand'. Analogous to nanim . In a pure (standalone) treatment of Nicod's axiom, this theorem would be changed to a definition ($a statement). (Contributed by NM, 11-Dec-2008) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion nic-dfim ⊢ φ ⊼ ψ ⊼ ψ ⊼ φ → ψ ⊼ φ ⊼ ψ ⊼ ψ ⊼ φ ⊼ ψ ⊼ ψ ⊼ φ → ψ ⊼ φ → ψ

Proof

Step Hyp Ref Expression
1 nanim ⊢ φ → ψ ↔ φ ⊼ ψ ⊼ ψ
2 1 bicomi ⊢ φ ⊼ ψ ⊼ ψ ↔ φ → ψ
3 nanbi ⊢ φ ⊼ ψ ⊼ ψ ↔ φ → ψ ↔ φ ⊼ ψ ⊼ ψ ⊼ φ → ψ ⊼ φ ⊼ ψ ⊼ ψ ⊼ φ ⊼ ψ ⊼ ψ ⊼ φ → ψ ⊼ φ → ψ
4 2 3 mpbi ⊢ φ ⊼ ψ ⊼ ψ ⊼ φ → ψ ⊼ φ ⊼ ψ ⊼ ψ ⊼ φ ⊼ ψ ⊼ ψ ⊼ φ → ψ ⊼ φ → ψ