Theorem ichan 48224

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 48215 instead of dfich2 48227 to reduce axioms. (Revised by SN, 4-May-2024.)

Assertion

Ref	Expression
ichan	⊢ (([𝑎⇄𝑏]𝜑 ∧ [𝑎⇄𝑏]𝜓) → [𝑎⇄𝑏](𝜑 ∧ 𝜓))

Proof of Theorem ichan

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		sban 2114	. . . . . . . 8 ⊢ ([𝑥 / 𝑏](𝜑 ∧ 𝜓) ↔ ([𝑥 / 𝑏]𝜑 ∧ [𝑥 / 𝑏]𝜓))
2	1	sbbii 2110	. . . . . . 7 ⊢ ([𝑏 / 𝑎][𝑥 / 𝑏](𝜑 ∧ 𝜓) ↔ [𝑏 / 𝑎]([𝑥 / 𝑏]𝜑 ∧ [𝑥 / 𝑏]𝜓))
3	2	sbbii 2110	. . . . . 6 ⊢ ([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏](𝜑 ∧ 𝜓) ↔ [𝑎 / 𝑥][𝑏 / 𝑎]([𝑥 / 𝑏]𝜑 ∧ [𝑥 / 𝑏]𝜓))
4		sban 2114	. . . . . . 7 ⊢ ([𝑏 / 𝑎]([𝑥 / 𝑏]𝜑 ∧ [𝑥 / 𝑏]𝜓) ↔ ([𝑏 / 𝑎][𝑥 / 𝑏]𝜑 ∧ [𝑏 / 𝑎][𝑥 / 𝑏]𝜓))
5	4	sbbii 2110	. . . . . 6 ⊢ ([𝑎 / 𝑥][𝑏 / 𝑎]([𝑥 / 𝑏]𝜑 ∧ [𝑥 / 𝑏]𝜓) ↔ [𝑎 / 𝑥]([𝑏 / 𝑎][𝑥 / 𝑏]𝜑 ∧ [𝑏 / 𝑎][𝑥 / 𝑏]𝜓))
6		sban 2114	. . . . . 6 ⊢ ([𝑎 / 𝑥]([𝑏 / 𝑎][𝑥 / 𝑏]𝜑 ∧ [𝑏 / 𝑎][𝑥 / 𝑏]𝜓) ↔ ([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜑 ∧ [𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜓))
7	3, 5, 6	3bitri 300	. . . . 5 ⊢ ([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏](𝜑 ∧ 𝜓) ↔ ([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜑 ∧ [𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜓))
8		pm4.38 648	. . . . 5 ⊢ ((([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜑 ↔ 𝜑) ∧ ([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜓 ↔ 𝜓)) → (([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜑 ∧ [𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜓) ↔ (𝜑 ∧ 𝜓)))
9	7, 8	bitrid 286	. . . 4 ⊢ ((([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜑 ↔ 𝜑) ∧ ([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜓 ↔ 𝜓)) → ([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏](𝜑 ∧ 𝜓) ↔ (𝜑 ∧ 𝜓)))
10	9	alanimi 1846	. . 3 ⊢ ((∀𝑏([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜑 ↔ 𝜑) ∧ ∀𝑏([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜓 ↔ 𝜓)) → ∀𝑏([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏](𝜑 ∧ 𝜓) ↔ (𝜑 ∧ 𝜓)))
11	10	alanimi 1846	. 2 ⊢ ((∀𝑎∀𝑏([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜑 ↔ 𝜑) ∧ ∀𝑎∀𝑏([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜓 ↔ 𝜓)) → ∀𝑎∀𝑏([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏](𝜑 ∧ 𝜓) ↔ (𝜑 ∧ 𝜓)))
12		df-ich 48215	. . 3 ⊢ ([𝑎⇄𝑏]𝜑 ↔ ∀𝑎∀𝑏([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜑 ↔ 𝜑))
13		df-ich 48215	. . 3 ⊢ ([𝑎⇄𝑏]𝜓 ↔ ∀𝑎∀𝑏([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜓 ↔ 𝜓))
14	12, 13	anbi12i 639	. 2 ⊢ (([𝑎⇄𝑏]𝜑 ∧ [𝑎⇄𝑏]𝜓) ↔ (∀𝑎∀𝑏([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜑 ↔ 𝜑) ∧ ∀𝑎∀𝑏([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜓 ↔ 𝜓)))
15		df-ich 48215	. 2 ⊢ ([𝑎⇄𝑏](𝜑 ∧ 𝜓) ↔ ∀𝑎∀𝑏([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏](𝜑 ∧ 𝜓) ↔ (𝜑 ∧ 𝜓)))
16	11, 14, 15	3imtr4i 295	1 ⊢ (([𝑎⇄𝑏]𝜑 ∧ [𝑎⇄𝑏]𝜓) → [𝑎⇄𝑏](𝜑 ∧ 𝜓))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400  ∀wal 1568  [wsb 2096  [wich 48214

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-sb 2097  df-ich 48215

This theorem is referenced by:  ichim  48226