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	|- ph

Assertion

Ref	Expression
idi	|- ph

Proof of Theorem idi

Step	Hyp	Ref	Expression
1		idi.1	1 |- ph

This theorem is referenced by:  opfi1uzindOLD  13289  madjusmdetlem2  29894  frege55lem2a  38161  fsovrfovd  38303  imo72b2lem0  38465  ssmapsn  39408  fprodcnlem  39831  limsupvaluz2  39970  dvmptfprod  40160  dvnprodlem1  40161  sge0f1o  40599  ovncvr2  40825  smfsupmpt  41021  smfinfmpt  41025  pfxcl  41386  rngcifuestrc  41997