Metamath Proof Explorer


Theorem e21

Description: A virtual deduction elimination rule (see syl6ci ). (Contributed by Alan Sare, 12-Jun-2011) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses e21.1 (    𝜑    ,    𝜓    ▶    𝜒    )
e21.2 (    𝜑    ▶    𝜃    )
e21.3 ( 𝜒 → ( 𝜃𝜏 ) )
Assertion e21 (    𝜑    ,    𝜓    ▶    𝜏    )

Proof

Step Hyp Ref Expression
1 e21.1 (    𝜑    ,    𝜓    ▶    𝜒    )
2 e21.2 (    𝜑    ▶    𝜃    )
3 e21.3 ( 𝜒 → ( 𝜃𝜏 ) )
4 2 vd12 (    𝜑    ,    𝜓    ▶    𝜃    )
5 1 4 3 e22 (    𝜑    ,    𝜓    ▶    𝜏    )