Theorem keephyp2v

Description: Keep a hypothesis containing 2 class variables (for use with the weak deduction theorem dedth ). (Contributed by NM, 16-Apr-2005)

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

Proof

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