Metamath Proof Explorer


Theorem dfvd2an

Description: Definition of a 2-hypothesis virtual deduction in vd conjunction form. (Contributed by Alan Sare, 23-Apr-2015) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion dfvd2an ( (    (    𝜑    ,    𝜓    )    ▶    𝜒    ) ↔ ( ( 𝜑𝜓 ) → 𝜒 ) )

Proof

Step Hyp Ref Expression
1 df-vd1 ( (    (    𝜑    ,    𝜓    )    ▶    𝜒    ) ↔ ( (    𝜑    ,    𝜓    )𝜒 ) )
2 df-vhc2 ( (    𝜑    ,    𝜓    ) ↔ ( 𝜑𝜓 ) )
3 2 imbi1i ( ( (    𝜑    ,    𝜓    )𝜒 ) ↔ ( ( 𝜑𝜓 ) → 𝜒 ) )
4 1 3 bitri ( (    (    𝜑    ,    𝜓    )    ▶    𝜒    ) ↔ ( ( 𝜑𝜓 ) → 𝜒 ) )