Theorem elimhyp2v

Description: Eliminate a hypothesis containing 2 class variables. (Contributed by NM, 14-Aug-1999)

	Ref	Expression
Hypotheses	elimhyp2v.1	$$⊢A=if\left(\phi ,A,C\right)\to \left(\phi \leftrightarrow \chi \right)$$
	elimhyp2v.2	$$⊢B=if\left(\phi ,B,D\right)\to \left(\chi \leftrightarrow \theta \right)$$
	elimhyp2v.3	$$⊢C=if\left(\phi ,A,C\right)\to \left(\tau \leftrightarrow \eta \right)$$
	elimhyp2v.4	$$⊢D=if\left(\phi ,B,D\right)\to \left(\eta \leftrightarrow \theta \right)$$
	elimhyp2v.5	$$⊢\tau$$
Assertion	elimhyp2v	$$⊢\theta$$

Proof

Step	Hyp	Ref	Expression
1		elimhyp2v.1	$$⊢A=if\left(\phi ,A,C\right)\to \left(\phi \leftrightarrow \chi \right)$$
2		elimhyp2v.2	$$⊢B=if\left(\phi ,B,D\right)\to \left(\chi \leftrightarrow \theta \right)$$
3		elimhyp2v.3	$$⊢C=if\left(\phi ,A,C\right)\to \left(\tau \leftrightarrow \eta \right)$$
4		elimhyp2v.4	$$⊢D=if\left(\phi ,B,D\right)\to \left(\eta \leftrightarrow \theta \right)$$
5		elimhyp2v.5	$$⊢\tau$$
6		iftrue	$$⊢\phi \to if\left(\phi ,A,C\right)=A$$
7	6	eqcomd	$$⊢\phi \to A=if\left(\phi ,A,C\right)$$
8	7 1	syl	$$⊢\phi \to \left(\phi \leftrightarrow \chi \right)$$
9		iftrue	$$⊢\phi \to if\left(\phi ,B,D\right)=B$$
10	9	eqcomd	$$⊢\phi \to B=if\left(\phi ,B,D\right)$$
11	10 2	syl	$$⊢\phi \to \left(\chi \leftrightarrow \theta \right)$$
12	8 11	bitrd	$$⊢\phi \to \left(\phi \leftrightarrow \theta \right)$$
13	12	ibi	$$⊢\phi \to \theta$$
14		iffalse	$$⊢\neg \phi \to if\left(\phi ,A,C\right)=C$$
15	14	eqcomd	$$⊢\neg \phi \to C=if\left(\phi ,A,C\right)$$
16	15 3	syl	$$⊢\neg \phi \to \left(\tau \leftrightarrow \eta \right)$$
17		iffalse	$$⊢\neg \phi \to if\left(\phi ,B,D\right)=D$$
18	17	eqcomd	$$⊢\neg \phi \to D=if\left(\phi ,B,D\right)$$
19	18 4	syl	$$⊢\neg \phi \to \left(\eta \leftrightarrow \theta \right)$$
20	16 19	bitrd	$$⊢\neg \phi \to \left(\tau \leftrightarrow \theta \right)$$
21	5 20	mpbii	$$⊢\neg \phi \to \theta$$
22	13 21	pm2.61i	$$⊢\theta$$