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:  opfi1uzindOLD  13284  madjusmdetlem2  29879  frege55lem2a  37987  fsovrfovd  38129  imo72b2lem0  38291  ssmapsn  39230  fprodcnlem  39637  limsupvaluz2  39776  dvmptfprod  39929  dvnprodlem1  39930  sge0f1o  40368  ovncvr2  40594  smfsupmpt  40790  smfinfmpt  40794  pfxcl  41157  rngcifuestrc  41768
  Copyright terms: Public domain W3C validator