Metamath Proof Explorer

Theorem naddlidd

Description: Identity law for natural addition. Deduction form. (Contributed by Scott Fenton, 30-Jul-2026)

Ref Expression
Hypothesis nadd.1 
|- ( ph -> A e. On )
Assertion naddlidd 
|- ( ph -> ( (/) +no A ) = A )

Proof

Step Hyp Ref Expression
1 nadd.1 
 |-  ( ph -> A e. On )
2 naddlid 
 |-  ( A e. On -> ( (/) +no A ) = A )
3 1 2 syl 
 |-  ( ph -> ( (/) +no A ) = A )