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

Theorem idiVD 28640
Description: Virtual deduction proof of idi 2. 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_ 28547  |-  ph
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
Hypothesis
Ref Expression
idiVD.1  |-  ph
Assertion
Ref Expression
idiVD  |-  ph

Proof of Theorem idiVD
StepHypRef Expression
1 idiVD.1 . 2  |-  ph
2 id 19 . 2  |-  ( ph  ->  ph )
31, 2e0_ 28547 1  |-  ph
Colors of variables: wff set class
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator