Theorem a1bi

Description: Inference introducing a theorem as an antecedent. (Contributed by NM, 5-Aug-1993) (Proof shortened by Wolf Lammen, 11-Nov-2012)

	Ref	Expression
Hypothesis	a1bi.1	⊢ 𝜑
Assertion	a1bi	⊢ ( 𝜓 ↔ ( 𝜑 → 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		a1bi.1	⊢ 𝜑
2		biimt	⊢ ( 𝜑 → ( 𝜓 ↔ ( 𝜑 → 𝜓 ) ) )
3	1 2	ax-mp	⊢ ( 𝜓 ↔ ( 𝜑 → 𝜓 ) )