Metamath Proof Explorer

Theorem hicli

Description: Closure inference for inner product. (Contributed by NM, 1-Aug-1999) (New usage is discouraged.)

Ref Expression
Hypotheses hicl.1 
|- A e. ~H
hicl.2 
|- B e. ~H
Assertion hicli 
|- ( A .ih B ) e. CC

Proof

Step Hyp Ref Expression
1 hicl.1 
 |-  A e. ~H
2 hicl.2 
 |-  B e. ~H
3 hicl 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( A .ih B ) e. CC )
4 1 2 3 mp2an 
 |-  ( A .ih B ) e. CC