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

Step	Hyp	Ref	Expression
1		idi.1	1 ⊢ 𝜑

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