MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  idi Structured version   Visualization version   GIF version

Theorem idi 2
Description: This inference, which requires no axioms for its proof, is useful as a copy-paste 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. It is the inference associated with id 22. (Contributed by Alan Sare, 31-Dec-2011.)
Ref Expression
idi.1 𝜑
Ref Expression
idi 𝜑

Proof of Theorem idi
StepHypRef Expression
1 idi.1 1 𝜑
Colors of variables: wff setvar class
This theorem is referenced by:  opfi1uzind  13138  opfi1uzindOLD  13144  opphllem2  25440  madjusmdetlem2  29222  frege55lem2a  37181  fsovrfovd  37323  imo72b2lem0  37487  ssmapsn  38403  fprodcnlem  38666  dvmptfprod  38835  dvnprodlem1  38836  sge0f1o  39275  ovncvr2  39501  pfxcl  40249  rngcifuestrc  41789
  Copyright terms: Public domain W3C validator