Theorem ichan

Description: If two setvar variables are interchangeable in two wffs, then they are interchangeable in the conjunction of these two wffs. Notice that the reverse implication is not necessarily true. Corresponding theorems will hold for other commutative operations, too. (Contributed by AV, 31-Jul-2023) Use df-ich instead of dfich2 to reduce axioms. (Revised by SN, 4-May-2024)

	Ref	Expression
Assertion	ichan	|- ( ( [ a <> b ] ph /\ [ a <> b ] ps ) -> [ a <> b ] ( ph /\ ps ) )

Proof

Step	Hyp	Ref	Expression
1		sban	|- ( [ x / b ] ( ph /\ ps ) <-> ( [ x / b ] ph /\ [ x / b ] ps ) )
2	1	sbbii	|- ( [ b / a ] [ x / b ] ( ph /\ ps ) <-> [ b / a ] ( [ x / b ] ph /\ [ x / b ] ps ) )
3	2	sbbii	|- ( [ a / x ] [ b / a ] [ x / b ] ( ph /\ ps ) <-> [ a / x ] [ b / a ] ( [ x / b ] ph /\ [ x / b ] ps ) )
4		sban	|- ( [ b / a ] ( [ x / b ] ph /\ [ x / b ] ps ) <-> ( [ b / a ] [ x / b ] ph /\ [ b / a ] [ x / b ] ps ) )
5	4	sbbii	|- ( [ a / x ] [ b / a ] ( [ x / b ] ph /\ [ x / b ] ps ) <-> [ a / x ] ( [ b / a ] [ x / b ] ph /\ [ b / a ] [ x / b ] ps ) )
6		sban	|- ( [ a / x ] ( [ b / a ] [ x / b ] ph /\ [ b / a ] [ x / b ] ps ) <-> ( [ a / x ] [ b / a ] [ x / b ] ph /\ [ a / x ] [ b / a ] [ x / b ] ps ) )
7	3 5 6	3bitri	|- ( [ a / x ] [ b / a ] [ x / b ] ( ph /\ ps ) <-> ( [ a / x ] [ b / a ] [ x / b ] ph /\ [ a / x ] [ b / a ] [ x / b ] ps ) )
8		pm4.38	|- ( ( ( [ a / x ] [ b / a ] [ x / b ] ph <-> ph ) /\ ( [ a / x ] [ b / a ] [ x / b ] ps <-> ps ) ) -> ( ( [ a / x ] [ b / a ] [ x / b ] ph /\ [ a / x ] [ b / a ] [ x / b ] ps ) <-> ( ph /\ ps ) ) )
9	7 8	bitrid	|- ( ( ( [ a / x ] [ b / a ] [ x / b ] ph <-> ph ) /\ ( [ a / x ] [ b / a ] [ x / b ] ps <-> ps ) ) -> ( [ a / x ] [ b / a ] [ x / b ] ( ph /\ ps ) <-> ( ph /\ ps ) ) )
10	9	alanimi	|- ( ( A. b ( [ a / x ] [ b / a ] [ x / b ] ph <-> ph ) /\ A. b ( [ a / x ] [ b / a ] [ x / b ] ps <-> ps ) ) -> A. b ( [ a / x ] [ b / a ] [ x / b ] ( ph /\ ps ) <-> ( ph /\ ps ) ) )
11	10	alanimi	|- ( ( A. a A. b ( [ a / x ] [ b / a ] [ x / b ] ph <-> ph ) /\ A. a A. b ( [ a / x ] [ b / a ] [ x / b ] ps <-> ps ) ) -> A. a A. b ( [ a / x ] [ b / a ] [ x / b ] ( ph /\ ps ) <-> ( ph /\ ps ) ) )
12		df-ich	|- ( [ a <> b ] ph <-> A. a A. b ( [ a / x ] [ b / a ] [ x / b ] ph <-> ph ) )
13		df-ich	|- ( [ a <> b ] ps <-> A. a A. b ( [ a / x ] [ b / a ] [ x / b ] ps <-> ps ) )
14	12 13	anbi12i	|- ( ( [ a <> b ] ph /\ [ a <> b ] ps ) <-> ( A. a A. b ( [ a / x ] [ b / a ] [ x / b ] ph <-> ph ) /\ A. a A. b ( [ a / x ] [ b / a ] [ x / b ] ps <-> ps ) ) )
15		df-ich	|- ( [ a <> b ] ( ph /\ ps ) <-> A. a A. b ( [ a / x ] [ b / a ] [ x / b ] ( ph /\ ps ) <-> ( ph /\ ps ) ) )
16	11 14 15	3imtr4i	|- ( ( [ a <> b ] ph /\ [ a <> b ] ps ) -> [ a <> b ] ( ph /\ ps ) )