Metamath Proof Explorer

Theorem naddridd

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 naddridd 
|- ( ph -> ( A +no (/) ) = A )

Proof

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