Theorem idi 2

Description: Inference form of id 19. 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. (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: (None)