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 28283 a9e2nd 28296 e233 28526 trsspwALT2 28581 sspwtrALT 28584 sstrALT2 28596 suctrALT3 28685 sspwimpALT 28686 a9e2ndALT 28692 a9e2ndeqALT 28693 
Copyright terms: Public domain  W3C validator 