Users' Mathboxes Mathbox for Alan Sare < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  idiVD Structured version   Visualization version   GIF version

Theorem idiVD 39599
Description: Virtual deduction proof of idiALT 39185. 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 39501 𝜑
(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
StepHypRef Expression
1 idiVD.1 . 2 𝜑
2 id 22 . 2 (𝜑𝜑)
31, 2e0a 39501 1 𝜑
Colors of variables: wff setvar class
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator