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	⊢ ( ( 𝜑 → 𝜓 ) ↔ ( 𝜑 ⊼ ( 𝜓 ⊼ 𝜓 ) ) )