Mathbox for Alan Sare 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > Mathboxes > iidn3  Structured version Unicode version 
Description: idn3 28617 without virtual deduction connectives. Special theorem needed for Alan Sare's virtual deduction translation tool. (Contributed by Alan Sare, 23Jul2011.) (Proof modification is discouraged.) (New usage is discouraged.) 
Ref  Expression 

iidn3 
Step  Hyp  Ref  Expression 

1  id 20  . 2  
2  1  a1ii 25  1 
Colors of variables: wff set class 
Syntax hints: wi 4 
This theorem is referenced by: trintALT 28894 
This theorem was proved from axioms: ax1 5 ax2 6 axmp 8 
Copyright terms: Public domain  W3C validator 