This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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	$⊢ ((φ, ψ) \to ψ)$

Proof

Step	Hyp	Ref	Expression
1		simpr	$⊢ (φ \land ψ) \to ψ$
2		dfvd2an	$⊢ ((φ, ψ) \to ψ) \leftrightarrow ((φ \land ψ) \to ψ)$
3	1 2	mpbir	$⊢ ((φ, ψ) \to ψ)$