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

Metamath Proof Explorer

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	$⊢ (φ \to ψ)$
	Assertion	vd13	$⊢ (φ, χ, θ \to ψ)$

Proof

Step	Hyp	Ref	Expression
1		vd13.1	$⊢ (φ \to ψ)$
2	1	in1	$⊢ φ \to ψ$
3	2	a1d	$⊢ φ \to (χ \to ψ)$
4	3	a1dd	$⊢ φ \to (χ \to (θ \to ψ))$
5	4	dfvd3ir	$⊢ (φ, χ, θ \to ψ)$