Mathbox for Alan Sare 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > Mathboxes > iidn3  Unicode version 
Description: idn3 27520 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 21  . 2  
2  1  a1ii 26  1 
Colors of variables: wff set class 
Syntax hints: wi 6 
This theorem is referenced by: trintALT 27790 
This theorem was proved from axioms: ax1 7 ax2 8 axmp 10 
Copyright terms: Public domain  W3C validator 