Theorem in1

Description: Inference form of df-vd1 . Virtual deduction introduction rule of converting the virtual hypothesis of a 1-virtual hypothesis virtual deduction into an antecedent. (Contributed by Alan Sare, 14-Nov-2011) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypothesis	in1.1	$$⊢\left(\phi \to \psi \right)$$
Assertion	in1	$$⊢\phi \to \psi$$

Proof

Step	Hyp	Ref	Expression
1		in1.1	$$⊢\left(\phi \to \psi \right)$$
2		df-vd1	$$⊢\left(\phi \to \psi \right)\leftrightarrow \left(\phi \to \psi \right)$$
3	1 2	mpbi	$$⊢\phi \to \psi$$