This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem elimph

Description: Hypothesis elimination lemma for complex inner product spaces to assist weak deduction theorem. (Contributed by NM, 27-Apr-2007) (New usage is discouraged.)

	Ref	Expression
Hypotheses	elimph.1	$⊢ X = BaseSet (U)$
	elimph.5	$⊢ Z = 0_{vec} (U)$
	elimph.6	$⊢ U \in {CPreHil}_{OLD}$
Assertion	elimph	$⊢ if (A \in X, A, Z) \in X$

Proof

Step	Hyp	Ref	Expression
1		elimph.1	$⊢ X = BaseSet (U)$
2		elimph.5	$⊢ Z = 0_{vec} (U)$
3		elimph.6	$⊢ U \in {CPreHil}_{OLD}$
4	3	phnvi	$⊢ U \in NrmCVec$
5	1 2 4	elimnv	$⊢ if (A \in X, A, Z) \in X$