Theorem elimhyp3v

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

	Ref	Expression
Hypotheses	elimhyp3v.1	$$⊢A=if\left(\phi ,A,D\right)\to \left(\phi \leftrightarrow \chi \right)$$
	elimhyp3v.2	$$⊢B=if\left(\phi ,B,R\right)\to \left(\chi \leftrightarrow \theta \right)$$
	elimhyp3v.3	$$⊢C=if\left(\phi ,C,S\right)\to \left(\theta \leftrightarrow \tau \right)$$
	elimhyp3v.4	$$⊢D=if\left(\phi ,A,D\right)\to \left(\eta \leftrightarrow \zeta \right)$$
	elimhyp3v.5	$$⊢R=if\left(\phi ,B,R\right)\to \left(\zeta \leftrightarrow \sigma \right)$$
	elimhyp3v.6	$$⊢S=if\left(\phi ,C,S\right)\to \left(\sigma \leftrightarrow \tau \right)$$
	elimhyp3v.7	$$⊢\eta$$
Assertion	elimhyp3v	$$⊢\tau$$

Proof

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