Theorem cbval2vOLD

Description: Obsolete version of cbval2v as of 14-Jan-2024. (Contributed by BJ, 16-Jan-2019) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	cbval2v.1	$$⊢Ⅎz\phi$$
	cbval2v.2	$$⊢Ⅎw\phi$$
	cbval2v.3	$$⊢Ⅎx\psi$$
	cbval2v.4	$$⊢Ⅎy\psi$$
	cbval2v.5	$$⊢\left(x=z\wedge y=w\right)\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	cbval2vOLD	$$⊢\forall x\forall y\phi \leftrightarrow \forall z\forall w\psi$$

Proof

Step	Hyp	Ref	Expression
1		cbval2v.1	$$⊢Ⅎz\phi$$
2		cbval2v.2	$$⊢Ⅎw\phi$$
3		cbval2v.3	$$⊢Ⅎx\psi$$
4		cbval2v.4	$$⊢Ⅎy\psi$$
5		cbval2v.5	$$⊢\left(x=z\wedge y=w\right)\to \left(\phi \leftrightarrow \psi \right)$$
6	1	nfal	$$⊢Ⅎz\forall y\phi$$
7	3	nfal	$$⊢Ⅎx\forall w\psi$$
8		nfv	$$⊢Ⅎwx=z$$
9	8 2	nfim	$$⊢Ⅎw\left(x=z\to \phi \right)$$
10		nfv	$$⊢Ⅎyx=z$$
11	10 4	nfim	$$⊢Ⅎy\left(x=z\to \psi \right)$$
12	5	expcom	$$⊢y=w\to \left(x=z\to \left(\phi \leftrightarrow \psi \right)\right)$$
13	12	pm5.74d	$$⊢y=w\to \left(\left(x=z\to \phi \right)\leftrightarrow \left(x=z\to \psi \right)\right)$$
14	9 11 13	cbvalv1	$$⊢\forall y\left(x=z\to \phi \right)\leftrightarrow \forall w\left(x=z\to \psi \right)$$
15		19.21v	$$⊢\forall y\left(x=z\to \phi \right)\leftrightarrow \left(x=z\to \forall y\phi \right)$$
16		19.21v	$$⊢\forall w\left(x=z\to \psi \right)\leftrightarrow \left(x=z\to \forall w\psi \right)$$
17	14 15 16	3bitr3i	$$⊢\left(x=z\to \forall y\phi \right)\leftrightarrow \left(x=z\to \forall w\psi \right)$$
18	17	pm5.74ri	$$⊢x=z\to \left(\forall y\phi \leftrightarrow \forall w\psi \right)$$
19	6 7 18	cbvalv1	$$⊢\forall x\forall y\phi \leftrightarrow \forall z\forall w\psi$$