Metamath Proof Explorer


Theorem iden2

Description: Virtual deduction identity rule. simpr in conjunction form Virtual Deduction notation. (Contributed by Alan Sare, 5-Sep-2016) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion iden2 (    (    𝜑    ,    𝜓    )    ▶    𝜓    )

Proof

Step Hyp Ref Expression
1 simpr ( ( 𝜑𝜓 ) → 𝜓 )
2 dfvd2an ( (    (    𝜑    ,    𝜓    )    ▶    𝜓    ) ↔ ( ( 𝜑𝜓 ) → 𝜓 ) )
3 1 2 mpbir (    (    𝜑    ,    𝜓    )    ▶    𝜓    )