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 28343 a9e2nd 28356 e233 28586 trsspwALT2 28641 sspwtrALT 28644 sstrALT2 28656 suctrALT3 28745 sspwimpALT 28746 a9e2ndALT 28752 a9e2ndeqALT 28753 
Copyright terms: Public domain  W3C validator 