Metamath Proof Explorer


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

Proof

Step Hyp Ref Expression
1 idALT
 |-  ( ph -> ph )