Theorem elimhyp

Description: Eliminate a hypothesis containing class variable A when it is known for a specific class B . For more information, see comments in dedth . (Contributed by NM, 15-May-1999)

	Ref	Expression
Hypotheses	elimhyp.1	$$⊢A=if\left(\phi ,A,B\right)\to \left(\phi \leftrightarrow \psi \right)$$
	elimhyp.2	$$⊢B=if\left(\phi ,A,B\right)\to \left(\chi \leftrightarrow \psi \right)$$
	elimhyp.3	$$⊢\chi$$
Assertion	elimhyp	$$⊢\psi$$

Proof

Step	Hyp	Ref	Expression
1		elimhyp.1	$$⊢A=if\left(\phi ,A,B\right)\to \left(\phi \leftrightarrow \psi \right)$$
2		elimhyp.2	$$⊢B=if\left(\phi ,A,B\right)\to \left(\chi \leftrightarrow \psi \right)$$
3		elimhyp.3	$$⊢\chi$$
4		iftrue	$$⊢\phi \to if\left(\phi ,A,B\right)=A$$
5	4	eqcomd	$$⊢\phi \to A=if\left(\phi ,A,B\right)$$
6	5 1	syl	$$⊢\phi \to \left(\phi \leftrightarrow \psi \right)$$
7	6	ibi	$$⊢\phi \to \psi$$
8		iffalse	$$⊢\neg \phi \to if\left(\phi ,A,B\right)=B$$
9	8	eqcomd	$$⊢\neg \phi \to B=if\left(\phi ,A,B\right)$$
10	9 2	syl	$$⊢\neg \phi \to \left(\chi \leftrightarrow \psi \right)$$
11	3 10	mpbii	$$⊢\neg \phi \to \psi$$
12	7 11	pm2.61i	$$⊢\psi$$