Theorem ifchhv

Description: Prove if ( A e. CH , A , ~H ) e. CH . (Contributed by David A. Wheeler, 8-Dec-2018) (New usage is discouraged.)

	Ref	Expression
Assertion	ifchhv	$$⊢if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\in {\mathbf{C}}_{\mathscr{H}}$$

Proof

Step	Hyp	Ref	Expression
1		helch	$$⊢\mathscr{H}\in {\mathbf{C}}_{\mathscr{H}}$$
2	1	elimel	$$⊢if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\in {\mathbf{C}}_{\mathscr{H}}$$