Metamath Proof Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > idi  Unicode version 
Description: Inference form of id 20. This inference rule, which requires no axioms for its proof, is useful as a copypaste mechanism during proof development in mmj2. It is normally not referenced in the final version of a proof, since it is always redundant and can be removed using the 'minimize *' command in the metamath program's Proof Assistant. (Contributed by Alan Sare, 31Dec2011.) 
Ref  Expression 

idi.1 
Ref  Expression 

idi 
Step  Hyp  Ref  Expression 

1  idi.1  1 
Colors of variables: wff set class 
This theorem is referenced by: onfrALTlem2 27977 a9e2nd 27990 e233 28220 trsspwALT2 28275 sspwtrALT 28278 sstrALT2 28290 suctrALT3 28379 sspwimpALT 28380 a9e2ndALT 28386 a9e2ndeqALT 28387 
Copyright terms: Public domain  W3C validator 