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	$⊢ (((φ ⊼ (ψ ⊼ ψ)) ⊼ (φ \to ψ)) ⊼ (((φ ⊼ (ψ ⊼ ψ)) ⊼ (φ ⊼ (ψ ⊼ ψ))) ⊼ ((φ \to ψ) ⊼ (φ \to ψ))))$

Proof

Step	Hyp	Ref	Expression
1		nanim	$⊢ (φ \to ψ) \leftrightarrow (φ ⊼ (ψ ⊼ ψ))$
2	1	bicomi	$⊢ (φ ⊼ (ψ ⊼ ψ)) \leftrightarrow (φ \to ψ)$
3		nanbi	$⊢ ((φ ⊼ (ψ ⊼ ψ)) \leftrightarrow (φ \to ψ)) \leftrightarrow (((φ ⊼ (ψ ⊼ ψ)) ⊼ (φ \to ψ)) ⊼ (((φ ⊼ (ψ ⊼ ψ)) ⊼ (φ ⊼ (ψ ⊼ ψ))) ⊼ ((φ \to ψ) ⊼ (φ \to ψ))))$
4	2 3	mpbi	$⊢ (((φ ⊼ (ψ ⊼ ψ)) ⊼ (φ \to ψ)) ⊼ (((φ ⊼ (ψ ⊼ ψ)) ⊼ (φ ⊼ (ψ ⊼ ψ))) ⊼ ((φ \to ψ) ⊼ (φ \to ψ))))$

Metamath Proof Explorer

Theorem nic-dfim

Proof