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

Metamath Proof Explorer

Theorem vd12

Description: A virtual deduction with 1 virtual hypothesis virtually inferring a virtual conclusion infers that the same conclusion is virtually inferred by the same virtual hypothesis and an additional hypothesis. (Contributed by Alan Sare, 12-Jun-2011) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Hypothesis	vd12.1	⊢ ( 𝜑 ▶ 𝜓 )
	Assertion	vd12	⊢ ( 𝜑 , 𝜒 ▶ 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		vd12.1	⊢ ( 𝜑 ▶ 𝜓 )
2	1	in1	⊢ ( 𝜑 → 𝜓 )
3	2	a1d	⊢ ( 𝜑 → ( 𝜒 → 𝜓 ) )
4	3	dfvd2ir	⊢ ( 𝜑 , 𝜒 ▶ 𝜓 )