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	$$⊢\left(\phi \to \psi \right)$$
Assertion	vd12	$$⊢\left(\phi ,\chi \to \psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		vd12.1	$$⊢\left(\phi \to \psi \right)$$
2	1	in1	$$⊢\phi \to \psi$$
3	2	a1d	$$⊢\phi \to \left(\chi \to \psi \right)$$
4	3	dfvd2ir	$$⊢\left(\phi ,\chi \to \psi \right)$$