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 (    𝜑    ,    𝜒    ▶    𝜓    )