Theorem elimhyp4v

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

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

Proof

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