Metamath Proof Explorer


Theorem vd02

Description: Two virtual hypotheses virtually infer a theorem. (Contributed by Alan Sare, 14-Jun-2011) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 vd02.1 𝜑
2 1 a1i ( 𝜒𝜑 )
3 2 a1i ( 𝜓 → ( 𝜒𝜑 ) )
4 3 dfvd2ir (    𝜓    ,    𝜒    ▶    𝜑    )