Theorem idiVD 38122

Description: Virtual deduction proof of idiALT 37704. The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.

h1::	⊢ 𝜑
qed:1,?: e0a 38020	⊢ 𝜑

(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypothesis

Ref	Expression
idiVD.1	⊢ 𝜑

Assertion

Ref	Expression
idiVD	⊢ 𝜑

Proof of Theorem idiVD

Step	Hyp	Ref	Expression
1		idiVD.1	. 2 ⊢ 𝜑
2		id 22	. 2 ⊢ (𝜑 → 𝜑)
3	1, 2	e0a 38020	1 ⊢ 𝜑

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by: (None)