Mathbox for Alan Sare 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > Mathboxes > idiVD  Structured version Unicode version 
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.

Ref  Expression 

idiVD.1 
Ref  Expression 

idiVD 
Step  Hyp  Ref  Expression 

1  idiVD.1  . 2  
2  id 20  . 2  
3  1, 2  e0_ 28884  1 
Colors of variables: wff set class 
This theorem was proved from axioms: ax1 5 ax2 6 axmp 8 
Copyright terms: Public domain  W3C validator 