Theorem ichan 48676

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 48667 instead of dfich2 48679 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 2118	. . . . . . . 8 ⊢ ([𝑥 / 𝑏](𝜑 ∧ 𝜓) ↔ ([𝑥 / 𝑏]𝜑 ∧ [𝑥 / 𝑏]𝜓))
2	1	sbbii 2114	. . . . . . 7 ⊢ ([𝑏 / 𝑎][𝑥 / 𝑏](𝜑 ∧ 𝜓) ↔ [𝑏 / 𝑎]([𝑥 / 𝑏]𝜑 ∧ [𝑥 / 𝑏]𝜓))
3	2	sbbii 2114	. . . . . 6 ⊢ ([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏](𝜑 ∧ 𝜓) ↔ [𝑎 / 𝑥][𝑏 / 𝑎]([𝑥 / 𝑏]𝜑 ∧ [𝑥 / 𝑏]𝜓))
4		sban 2118	. . . . . . 7 ⊢ ([𝑏 / 𝑎]([𝑥 / 𝑏]𝜑 ∧ [𝑥 / 𝑏]𝜓) ↔ ([𝑏 / 𝑎][𝑥 / 𝑏]𝜑 ∧ [𝑏 / 𝑎][𝑥 / 𝑏]𝜓))
5	4	sbbii 2114	. . . . . 6 ⊢ ([𝑎 / 𝑥][𝑏 / 𝑎]([𝑥 / 𝑏]𝜑 ∧ [𝑥 / 𝑏]𝜓) ↔ [𝑎 / 𝑥]([𝑏 / 𝑎][𝑥 / 𝑏]𝜑 ∧ [𝑏 / 𝑎][𝑥 / 𝑏]𝜓))
6		sban 2118	. . . . . 6 ⊢ ([𝑎 / 𝑥]([𝑏 / 𝑎][𝑥 / 𝑏]𝜑 ∧ [𝑏 / 𝑎][𝑥 / 𝑏]𝜓) ↔ ([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜑 ∧ [𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜓))
7	3, 5, 6	3bitri 300	. . . . 5 ⊢ ([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏](𝜑 ∧ 𝜓) ↔ ([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜑 ∧ [𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜓))
8		pm4.38 649	. . . . 5 ⊢ ((([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜑 ↔ 𝜑) ∧ ([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜓 ↔ 𝜓)) → (([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜑 ∧ [𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜓) ↔ (𝜑 ∧ 𝜓)))
9	7, 8	bitrid 286	. . . 4 ⊢ ((([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜑 ↔ 𝜑) ∧ ([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜓 ↔ 𝜓)) → ([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏](𝜑 ∧ 𝜓) ↔ (𝜑 ∧ 𝜓)))
10	9	alanimi 1848	. . 3 ⊢ ((∀𝑏([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜑 ↔ 𝜑) ∧ ∀𝑏([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜓 ↔ 𝜓)) → ∀𝑏([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏](𝜑 ∧ 𝜓) ↔ (𝜑 ∧ 𝜓)))
11	10	alanimi 1848	. 2 ⊢ ((∀𝑎∀𝑏([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜑 ↔ 𝜑) ∧ ∀𝑎∀𝑏([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜓 ↔ 𝜓)) → ∀𝑎∀𝑏([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏](𝜑 ∧ 𝜓) ↔ (𝜑 ∧ 𝜓)))
12		df-ich 48667	. . 3 ⊢ ([𝑎⇄𝑏]𝜑 ↔ ∀𝑎∀𝑏([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜑 ↔ 𝜑))
13		df-ich 48667	. . 3 ⊢ ([𝑎⇄𝑏]𝜓 ↔ ∀𝑎∀𝑏([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜓 ↔ 𝜓))
14	12, 13	anbi12i 640	. 2 ⊢ (([𝑎⇄𝑏]𝜑 ∧ [𝑎⇄𝑏]𝜓) ↔ (∀𝑎∀𝑏([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜑 ↔ 𝜑) ∧ ∀𝑎∀𝑏([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜓 ↔ 𝜓)))
15		df-ich 48667	. 2 ⊢ ([𝑎⇄𝑏](𝜑 ∧ 𝜓) ↔ ∀𝑎∀𝑏([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏](𝜑 ∧ 𝜓) ↔ (𝜑 ∧ 𝜓)))
16	11, 14, 15	3imtr4i 295	1 ⊢ (([𝑎⇄𝑏]𝜑 ∧ [𝑎⇄𝑏]𝜓) → [𝑎⇄𝑏](𝜑 ∧ 𝜓))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1567  [wsb 2100  [wich 48666

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2101  df-ich 48667

This theorem is used by:  ichim  48678