Metamath Proof Explorer


Theorem addcli

Description: Closure law for addition. (Contributed by NM, 23-Nov-1994)

Ref Expression
Hypotheses axi.1 A
axi.2 B
Assertion addcli A + B

Proof

Step Hyp Ref Expression
1 axi.1 A
2 axi.2 B
3 addcl A B A + B
4 1 2 3 mp2an A + B