Mathbox for Alan Sare 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > Mathboxes > idiVD  Structured version Visualization version GIF version 
Description: Virtual deduction proof of idiALT 41034. 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 22  . 2 ⊢ (𝜑 → 𝜑)  
3  1, 2  e0a 41329  1 ⊢ 𝜑 
Colors of variables: wff setvar class 
This theorem was proved from axioms: axmp 5 ax1 6 ax2 7 
This theorem is referenced by: (None) 
Copyright terms: Public domain  W3C validator 