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	$$⊢\left(\left(\phi ,\psi \right)\to \psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		simpr	$$⊢\left(\phi \wedge \psi \right)\to \psi$$
2		dfvd2an	$$⊢\left(\left(\phi ,\psi \right)\to \psi \right)\leftrightarrow \left(\left(\phi \wedge \psi \right)\to \psi \right)$$
3	1 2	mpbir	$$⊢\left(\left(\phi ,\psi \right)\to \psi \right)$$