Theorem ichan 47643

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1539  [wsb 2067  [wich 47633

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-ich 47634

This theorem is referenced by:  ichim  47645