Theorem elimel

Description: Eliminate a membership hypothesis for weak deduction theorem, when special case B e. C is provable. (Contributed by NM, 15-May-1999)

	Ref	Expression
Hypothesis	elimel.1	$$⊢B\in C$$
Assertion	elimel	$$⊢if\left(A\in C,A,B\right)\in C$$

Proof

Step	Hyp	Ref	Expression
1		elimel.1	$$⊢B\in C$$
2		eleq1	$$⊢A=if\left(A\in C,A,B\right)\to \left(A\in C\leftrightarrow if\left(A\in C,A,B\right)\in C\right)$$
3		eleq1	$$⊢B=if\left(A\in C,A,B\right)\to \left(B\in C\leftrightarrow if\left(A\in C,A,B\right)\in C\right)$$
4	2 3 1	elimhyp	$$⊢if\left(A\in C,A,B\right)\in C$$