Theorem idiVD 16688

Description: Virtual deduction proof of idi 1290. 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::	|- ph
qed:1,?: e0_ 16637	|- ph

Hypothesis

Ref	Expression
idiVD.1	|- ph

Assertion

Ref	Expression
idiVD	|- ph

Proof of Theorem idiVD

Step	Hyp	Ref	Expression
1		idiVD.1	. 2 |- ph
2		id 73	. 2 |- (ph -> ph)
3	1, 2	e0_ 16637	1 |- ph

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

Copyright terms: Public domain