Theorem cjcli

Description: Closure law for complex conjugate. (Contributed by NM, 11-May-1999)

	Ref	Expression
Hypothesis	recl.1	$$⊢A\in ℂ$$
Assertion	cjcli	$$⊢\bar{A}\in ℂ$$

Proof

Step	Hyp	Ref	Expression
1		recl.1	$$⊢A\in ℂ$$
2		cjcl	$$⊢A\in ℂ\to \bar{A}\in ℂ$$
3	1 2	ax-mp	$$⊢\bar{A}\in ℂ$$