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	|- F/ z ph
	cbval2v.2	|- F/ w ph
	cbval2v.3	|- F/ x ps
	cbval2v.4	|- F/ y ps
	cbval2v.5	|- ( ( x = z /\ y = w ) -> ( ph <-> ps ) )
Assertion	cbval2vOLD	|- ( A. x A. y ph <-> A. z A. w ps )

Proof

Step	Hyp	Ref	Expression
1		cbval2v.1	|- F/ z ph
2		cbval2v.2	|- F/ w ph
3		cbval2v.3	|- F/ x ps
4		cbval2v.4	|- F/ y ps
5		cbval2v.5	|- ( ( x = z /\ y = w ) -> ( ph <-> ps ) )
6	1	nfal	|- F/ z A. y ph
7	3	nfal	|- F/ x A. w ps
8		nfv	|- F/ w x = z
9	8 2	nfim	|- F/ w ( x = z -> ph )
10		nfv	|- F/ y x = z
11	10 4	nfim	|- F/ y ( x = z -> ps )
12	5	expcom	|- ( y = w -> ( x = z -> ( ph <-> ps ) ) )
13	12	pm5.74d	|- ( y = w -> ( ( x = z -> ph ) <-> ( x = z -> ps ) ) )
14	9 11 13	cbvalv1	|- ( A. y ( x = z -> ph ) <-> A. w ( x = z -> ps ) )
15		19.21v	|- ( A. y ( x = z -> ph ) <-> ( x = z -> A. y ph ) )
16		19.21v	|- ( A. w ( x = z -> ps ) <-> ( x = z -> A. w ps ) )
17	14 15 16	3bitr3i	|- ( ( x = z -> A. y ph ) <-> ( x = z -> A. w ps ) )
18	17	pm5.74ri	|- ( x = z -> ( A. y ph <-> A. w ps ) )
19	6 7 18	cbvalv1	|- ( A. x A. y ph <-> A. z A. w ps )