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.)
Hypothesis
Ref Expression
idi.1 𝜑
Assertion
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  13238  opfi1uzindOLD  13244  opphllem2  25574  madjusmdetlem2  29718  frege55lem2a  37682  fsovrfovd  37824  imo72b2lem0  37986  ssmapsn  38917  fprodcnlem  39267  limsupvaluz2  39406  dvmptfprod  39497  dvnprodlem1  39498  sge0f1o  39936  ovncvr2  40162  smfsupmpt  40358  smfinfmpt  40362  pfxcl  40715  rngcifuestrc  41315
  Copyright terms: Public domain W3C validator