Theorem ichan 46123

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397  ∀wal 1540  [wsb 2068  [wich 46113

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

This theorem depends on definitions:  df-bi 206  df-an 398  df-sb 2069  df-ich 46114

This theorem is referenced by:  ichim  46125