Theorem idi 2

Description: Inference form of id 22. This inference rule, 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. Contrary to its closed form id 22, it requires no axioms for its proof. (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:  opphllem2  24120  dvmptfprod  31742  dvnprodlem1  31743  rngcifuestrc  32805  frege55lem2a  37894  imo72b2lem0  37982