Metamath Proof Explorer


Theorem vd03

Description: A theorem is virtually inferred by the 3 virtual hypotheses. (Contributed by Alan Sare, 12-Jun-2011) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 vd03.1 𝜑
2 1 a1i ( 𝜃𝜑 )
3 2 a1i ( 𝜒 → ( 𝜃𝜑 ) )
4 3 a1i ( 𝜓 → ( 𝜒 → ( 𝜃𝜑 ) ) )
5 4 dfvd3ir (    𝜓    ,    𝜒    ,    𝜃    ▶    𝜑    )