Mathbox for Alan Sare 
< Previous
Next >
Nearby theorems 

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