Theorem id1

Description: Alias for idALT that may be referenced in some older works, and kept here to prevent broken links.

If you landed here, please let the originating site and/or us know that the link that made you land here should be changed to a link to idALT .

(Contributed by NM, 30-Sep-1992) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	id1	⊢ ( 𝜑 → 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		idALT	⊢ ( 𝜑 → 𝜑 )