Theorem wl-2spsbbi

Description: spsbbi applied twice. (Contributed by Wolf Lammen, 5-Aug-2023)

	Ref	Expression
Assertion	wl-2spsbbi	|- ( A. a A. b ( ph <-> ps ) -> ( [ y / b ] [ x / a ] ph <-> [ y / b ] [ x / a ] ps ) )

Proof

Step	Hyp	Ref	Expression
1		alcom	|- ( A. a A. b ( ph <-> ps ) <-> A. b A. a ( ph <-> ps ) )
2		nfa1	|- F/ b A. b A. a ( ph <-> ps )
3		nfa1	|- F/ a A. a ( ph <-> ps )
4		sp	|- ( A. a ( ph <-> ps ) -> ( ph <-> ps ) )
5	3 4	sbbid	|- ( A. a ( ph <-> ps ) -> ( [ x / a ] ph <-> [ x / a ] ps ) )
6	5	sps	|- ( A. b A. a ( ph <-> ps ) -> ( [ x / a ] ph <-> [ x / a ] ps ) )
7	2 6	sbbid	|- ( A. b A. a ( ph <-> ps ) -> ( [ y / b ] [ x / a ] ph <-> [ y / b ] [ x / a ] ps ) )
8	1 7	sylbi	|- ( A. a A. b ( ph <-> ps ) -> ( [ y / b ] [ x / a ] ph <-> [ y / b ] [ x / a ] ps ) )