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	$$⊢\phi$$
Assertion	a1bi	$$⊢\psi \leftrightarrow \left(\phi \to \psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		a1bi.1	$$⊢\phi$$
2		biimt	$$⊢\phi \to \left(\psi \leftrightarrow \left(\phi \to \psi \right)\right)$$
3	1 2	ax-mp	$$⊢\psi \leftrightarrow \left(\phi \to \psi \right)$$