Theorem keephyp3v

Description: Keep a hypothesis containing 3 class variables. (Contributed by NM, 27-Sep-1999)

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

Proof

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