This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	⊢ ( 𝜑 ▶ 𝜓 )
	Assertion	in1	⊢ ( 𝜑 → 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		in1.1	⊢ ( 𝜑 ▶ 𝜓 )
2		df-vd1	⊢ ( ( 𝜑 ▶ 𝜓 ) ↔ ( 𝜑 → 𝜓 ) )
3	1 2	mpbi	⊢ ( 𝜑 → 𝜓 )