Metamath Proof Explorer

Theorem cjcli

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

Ref Expression
Hypothesis recl.1 
|- A e. CC
Assertion cjcli 
|- ( * ` A ) e. CC

Proof

Step Hyp Ref Expression
1 recl.1 
 |-  A e. CC
2 cjcl 
 |-  ( A e. CC -> ( * ` A ) e. CC )
3 1 2 ax-mp 
 |-  ( * ` A ) e. CC