Theorem addcl

Description: Alias for ax-addcl , for naming consistency with addcli . Use this theorem instead of ax-addcl or axaddcl . (Contributed by NM, 10-Mar-2008)

	Ref	Expression
Assertion	addcl	|- ( ( A e. CC /\ B e. CC ) -> ( A + B ) e. CC )

Proof

Step	Hyp	Ref	Expression
1		ax-addcl	|- ( ( A e. CC /\ B e. CC ) -> ( A + B ) e. CC )