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 "MM-PA> MINIMIZEWITH *" command in the Metamath program Proof Assistant. It is the inference associated with id 22. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
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:  wspthnonOLD  27007  madjusmdetlem2  30242  frege55lem2a  38679  fsovrfovd  38821  imo72b2lem0  38983  ssmapsn  39913  fprodcnlem  40329  limsupvaluz2  40468  dvmptfprod  40658  dvnprodlem1  40659  sge0f1o  41096  ovncvr2  41325  smfsupmpt  41521  smfinfmpt  41525  pfxcl  41979  rngcifuestrc  42583
  Copyright terms: Public domain W3C validator