Theorem vd13

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 a two additional hypotheses. (Contributed by Alan Sare, 12-Jun-2011) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		vd13.1	⊢ (    𝜑    ▶    𝜓    )
2	1	in1	⊢ ( 𝜑 → 𝜓 )
3	2	a1d	⊢ ( 𝜑 → ( 𝜒 → 𝜓 ) )
4	3	a1dd	⊢ ( 𝜑 → ( 𝜒 → ( 𝜃 → 𝜓 ) ) )
5	4	dfvd3ir	⊢ (    𝜑    ,    𝜒    ,    𝜃    ▶    𝜓    )