Theorem ichan 47460

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 47451 instead of dfich2 47463 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 2081	. . . . . . . 8 ⊢ ([𝑥 / 𝑏](𝜑 ∧ 𝜓) ↔ ([𝑥 / 𝑏]𝜑 ∧ [𝑥 / 𝑏]𝜓))
2	1	sbbii 2077	. . . . . . 7 ⊢ ([𝑏 / 𝑎][𝑥 / 𝑏](𝜑 ∧ 𝜓) ↔ [𝑏 / 𝑎]([𝑥 / 𝑏]𝜑 ∧ [𝑥 / 𝑏]𝜓))
3	2	sbbii 2077	. . . . . 6 ⊢ ([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏](𝜑 ∧ 𝜓) ↔ [𝑎 / 𝑥][𝑏 / 𝑎]([𝑥 / 𝑏]𝜑 ∧ [𝑥 / 𝑏]𝜓))
4		sban 2081	. . . . . . 7 ⊢ ([𝑏 / 𝑎]([𝑥 / 𝑏]𝜑 ∧ [𝑥 / 𝑏]𝜓) ↔ ([𝑏 / 𝑎][𝑥 / 𝑏]𝜑 ∧ [𝑏 / 𝑎][𝑥 / 𝑏]𝜓))
5	4	sbbii 2077	. . . . . 6 ⊢ ([𝑎 / 𝑥][𝑏 / 𝑎]([𝑥 / 𝑏]𝜑 ∧ [𝑥 / 𝑏]𝜓) ↔ [𝑎 / 𝑥]([𝑏 / 𝑎][𝑥 / 𝑏]𝜑 ∧ [𝑏 / 𝑎][𝑥 / 𝑏]𝜓))
6		sban 2081	. . . . . 6 ⊢ ([𝑎 / 𝑥]([𝑏 / 𝑎][𝑥 / 𝑏]𝜑 ∧ [𝑏 / 𝑎][𝑥 / 𝑏]𝜓) ↔ ([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜑 ∧ [𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜓))
7	3, 5, 6	3bitri 297	. . . . 5 ⊢ ([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏](𝜑 ∧ 𝜓) ↔ ([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜑 ∧ [𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜓))
8		pm4.38 637	. . . . 5 ⊢ ((([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜑 ↔ 𝜑) ∧ ([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜓 ↔ 𝜓)) → (([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜑 ∧ [𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜓) ↔ (𝜑 ∧ 𝜓)))
9	7, 8	bitrid 283	. . . 4 ⊢ ((([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜑 ↔ 𝜑) ∧ ([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜓 ↔ 𝜓)) → ([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏](𝜑 ∧ 𝜓) ↔ (𝜑 ∧ 𝜓)))
10	9	alanimi 1816	. . 3 ⊢ ((∀𝑏([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜑 ↔ 𝜑) ∧ ∀𝑏([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜓 ↔ 𝜓)) → ∀𝑏([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏](𝜑 ∧ 𝜓) ↔ (𝜑 ∧ 𝜓)))
11	10	alanimi 1816	. 2 ⊢ ((∀𝑎∀𝑏([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜑 ↔ 𝜑) ∧ ∀𝑎∀𝑏([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜓 ↔ 𝜓)) → ∀𝑎∀𝑏([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏](𝜑 ∧ 𝜓) ↔ (𝜑 ∧ 𝜓)))
12		df-ich 47451	. . 3 ⊢ ([𝑎⇄𝑏]𝜑 ↔ ∀𝑎∀𝑏([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜑 ↔ 𝜑))
13		df-ich 47451	. . 3 ⊢ ([𝑎⇄𝑏]𝜓 ↔ ∀𝑎∀𝑏([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜓 ↔ 𝜓))
14	12, 13	anbi12i 628	. 2 ⊢ (([𝑎⇄𝑏]𝜑 ∧ [𝑎⇄𝑏]𝜓) ↔ (∀𝑎∀𝑏([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜑 ↔ 𝜑) ∧ ∀𝑎∀𝑏([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜓 ↔ 𝜓)))
15		df-ich 47451	. 2 ⊢ ([𝑎⇄𝑏](𝜑 ∧ 𝜓) ↔ ∀𝑎∀𝑏([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏](𝜑 ∧ 𝜓) ↔ (𝜑 ∧ 𝜓)))
16	11, 14, 15	3imtr4i 292	1 ⊢ (([𝑎⇄𝑏]𝜑 ∧ [𝑎⇄𝑏]𝜓) → [𝑎⇄𝑏](𝜑 ∧ 𝜓))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1538  [wsb 2065  [wich 47450

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809

This theorem depends on definitions:  df-bi 207  df-an 396  df-sb 2066  df-ich 47451

This theorem is referenced by:  ichim  47462