|Metamath Proof Explorer||
|Mirrors > Home > MPE Home > Th. List > id1||Structured version Visualization version GIF version|
|Description: Alias for idALT 23
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 23.
(Contributed by NM, 30-Sep-1992.) (Proof modification is discouraged.) (New usage is discouraged.)
|id1||⊢ (𝜑 → 𝜑)|
|1||idALT 23||1 ⊢ (𝜑 → 𝜑)|
|Colors of variables: wff setvar class|
|Syntax hints: → wi 4|
|This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7|
|This theorem is referenced by: (None)|
|Copyright terms: Public domain||W3C validator|