Theorem ichan 43704

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.)

Assertion

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

Distinct variable group:   𝑎,𝑏

Allowed substitution hints:   𝜑(𝑎,𝑏)   𝜓(𝑎,𝑏)

Proof of Theorem ichan

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		19.26-2 1871	. . . 4 ⊢ (∀𝑥∀𝑦(([𝑥 / 𝑎][𝑦 / 𝑏]𝜑 ↔ [𝑦 / 𝑎][𝑥 / 𝑏]𝜑) ∧ ([𝑥 / 𝑎][𝑦 / 𝑏]𝜓 ↔ [𝑦 / 𝑎][𝑥 / 𝑏]𝜓)) ↔ (∀𝑥∀𝑦([𝑥 / 𝑎][𝑦 / 𝑏]𝜑 ↔ [𝑦 / 𝑎][𝑥 / 𝑏]𝜑) ∧ ∀𝑥∀𝑦([𝑥 / 𝑎][𝑦 / 𝑏]𝜓 ↔ [𝑦 / 𝑎][𝑥 / 𝑏]𝜓)))
2		pm4.38 636	. . . . . . . 8 ⊢ ((([𝑥 / 𝑎][𝑦 / 𝑏]𝜑 ↔ [𝑦 / 𝑎][𝑥 / 𝑏]𝜑) ∧ ([𝑥 / 𝑎][𝑦 / 𝑏]𝜓 ↔ [𝑦 / 𝑎][𝑥 / 𝑏]𝜓)) → (([𝑥 / 𝑎][𝑦 / 𝑏]𝜑 ∧ [𝑥 / 𝑎][𝑦 / 𝑏]𝜓) ↔ ([𝑦 / 𝑎][𝑥 / 𝑏]𝜑 ∧ [𝑦 / 𝑎][𝑥 / 𝑏]𝜓)))
3	2	biimpd 231	. . . . . . 7 ⊢ ((([𝑥 / 𝑎][𝑦 / 𝑏]𝜑 ↔ [𝑦 / 𝑎][𝑥 / 𝑏]𝜑) ∧ ([𝑥 / 𝑎][𝑦 / 𝑏]𝜓 ↔ [𝑦 / 𝑎][𝑥 / 𝑏]𝜓)) → (([𝑥 / 𝑎][𝑦 / 𝑏]𝜑 ∧ [𝑥 / 𝑎][𝑦 / 𝑏]𝜓) → ([𝑦 / 𝑎][𝑥 / 𝑏]𝜑 ∧ [𝑦 / 𝑎][𝑥 / 𝑏]𝜓)))
4		sban 2085	. . . . . . . . 9 ⊢ ([𝑦 / 𝑏](𝜑 ∧ 𝜓) ↔ ([𝑦 / 𝑏]𝜑 ∧ [𝑦 / 𝑏]𝜓))
5	4	sbbii 2080	. . . . . . . 8 ⊢ ([𝑥 / 𝑎][𝑦 / 𝑏](𝜑 ∧ 𝜓) ↔ [𝑥 / 𝑎]([𝑦 / 𝑏]𝜑 ∧ [𝑦 / 𝑏]𝜓))
6		sban 2085	. . . . . . . 8 ⊢ ([𝑥 / 𝑎]([𝑦 / 𝑏]𝜑 ∧ [𝑦 / 𝑏]𝜓) ↔ ([𝑥 / 𝑎][𝑦 / 𝑏]𝜑 ∧ [𝑥 / 𝑎][𝑦 / 𝑏]𝜓))
7	5, 6	bitri 277	. . . . . . 7 ⊢ ([𝑥 / 𝑎][𝑦 / 𝑏](𝜑 ∧ 𝜓) ↔ ([𝑥 / 𝑎][𝑦 / 𝑏]𝜑 ∧ [𝑥 / 𝑎][𝑦 / 𝑏]𝜓))
8		sban 2085	. . . . . . . . 9 ⊢ ([𝑥 / 𝑏](𝜑 ∧ 𝜓) ↔ ([𝑥 / 𝑏]𝜑 ∧ [𝑥 / 𝑏]𝜓))
9	8	sbbii 2080	. . . . . . . 8 ⊢ ([𝑦 / 𝑎][𝑥 / 𝑏](𝜑 ∧ 𝜓) ↔ [𝑦 / 𝑎]([𝑥 / 𝑏]𝜑 ∧ [𝑥 / 𝑏]𝜓))
10		sban 2085	. . . . . . . 8 ⊢ ([𝑦 / 𝑎]([𝑥 / 𝑏]𝜑 ∧ [𝑥 / 𝑏]𝜓) ↔ ([𝑦 / 𝑎][𝑥 / 𝑏]𝜑 ∧ [𝑦 / 𝑎][𝑥 / 𝑏]𝜓))
11	9, 10	bitri 277	. . . . . . 7 ⊢ ([𝑦 / 𝑎][𝑥 / 𝑏](𝜑 ∧ 𝜓) ↔ ([𝑦 / 𝑎][𝑥 / 𝑏]𝜑 ∧ [𝑦 / 𝑎][𝑥 / 𝑏]𝜓))
12	3, 7, 11	3imtr4g 298	. . . . . 6 ⊢ ((([𝑥 / 𝑎][𝑦 / 𝑏]𝜑 ↔ [𝑦 / 𝑎][𝑥 / 𝑏]𝜑) ∧ ([𝑥 / 𝑎][𝑦 / 𝑏]𝜓 ↔ [𝑦 / 𝑎][𝑥 / 𝑏]𝜓)) → ([𝑥 / 𝑎][𝑦 / 𝑏](𝜑 ∧ 𝜓) → [𝑦 / 𝑎][𝑥 / 𝑏](𝜑 ∧ 𝜓)))
13	12	2alimi 1812	. . . . 5 ⊢ (∀𝑥∀𝑦(([𝑥 / 𝑎][𝑦 / 𝑏]𝜑 ↔ [𝑦 / 𝑎][𝑥 / 𝑏]𝜑) ∧ ([𝑥 / 𝑎][𝑦 / 𝑏]𝜓 ↔ [𝑦 / 𝑎][𝑥 / 𝑏]𝜓)) → ∀𝑥∀𝑦([𝑥 / 𝑎][𝑦 / 𝑏](𝜑 ∧ 𝜓) → [𝑦 / 𝑎][𝑥 / 𝑏](𝜑 ∧ 𝜓)))
14		bicom1 223	. . . . . . . . 9 ⊢ (([𝑥 / 𝑎][𝑦 / 𝑏]𝜑 ↔ [𝑦 / 𝑎][𝑥 / 𝑏]𝜑) → ([𝑦 / 𝑎][𝑥 / 𝑏]𝜑 ↔ [𝑥 / 𝑎][𝑦 / 𝑏]𝜑))
15		bicom1 223	. . . . . . . . 9 ⊢ (([𝑥 / 𝑎][𝑦 / 𝑏]𝜓 ↔ [𝑦 / 𝑎][𝑥 / 𝑏]𝜓) → ([𝑦 / 𝑎][𝑥 / 𝑏]𝜓 ↔ [𝑥 / 𝑎][𝑦 / 𝑏]𝜓))
16	14, 15	bi2anan9 637	. . . . . . . 8 ⊢ ((([𝑥 / 𝑎][𝑦 / 𝑏]𝜑 ↔ [𝑦 / 𝑎][𝑥 / 𝑏]𝜑) ∧ ([𝑥 / 𝑎][𝑦 / 𝑏]𝜓 ↔ [𝑦 / 𝑎][𝑥 / 𝑏]𝜓)) → (([𝑦 / 𝑎][𝑥 / 𝑏]𝜑 ∧ [𝑦 / 𝑎][𝑥 / 𝑏]𝜓) ↔ ([𝑥 / 𝑎][𝑦 / 𝑏]𝜑 ∧ [𝑥 / 𝑎][𝑦 / 𝑏]𝜓)))
17	16	biimpd 231	. . . . . . 7 ⊢ ((([𝑥 / 𝑎][𝑦 / 𝑏]𝜑 ↔ [𝑦 / 𝑎][𝑥 / 𝑏]𝜑) ∧ ([𝑥 / 𝑎][𝑦 / 𝑏]𝜓 ↔ [𝑦 / 𝑎][𝑥 / 𝑏]𝜓)) → (([𝑦 / 𝑎][𝑥 / 𝑏]𝜑 ∧ [𝑦 / 𝑎][𝑥 / 𝑏]𝜓) → ([𝑥 / 𝑎][𝑦 / 𝑏]𝜑 ∧ [𝑥 / 𝑎][𝑦 / 𝑏]𝜓)))
18	17, 11, 7	3imtr4g 298	. . . . . 6 ⊢ ((([𝑥 / 𝑎][𝑦 / 𝑏]𝜑 ↔ [𝑦 / 𝑎][𝑥 / 𝑏]𝜑) ∧ ([𝑥 / 𝑎][𝑦 / 𝑏]𝜓 ↔ [𝑦 / 𝑎][𝑥 / 𝑏]𝜓)) → ([𝑦 / 𝑎][𝑥 / 𝑏](𝜑 ∧ 𝜓) → [𝑥 / 𝑎][𝑦 / 𝑏](𝜑 ∧ 𝜓)))
19	18	2alimi 1812	. . . . 5 ⊢ (∀𝑥∀𝑦(([𝑥 / 𝑎][𝑦 / 𝑏]𝜑 ↔ [𝑦 / 𝑎][𝑥 / 𝑏]𝜑) ∧ ([𝑥 / 𝑎][𝑦 / 𝑏]𝜓 ↔ [𝑦 / 𝑎][𝑥 / 𝑏]𝜓)) → ∀𝑥∀𝑦([𝑦 / 𝑎][𝑥 / 𝑏](𝜑 ∧ 𝜓) → [𝑥 / 𝑎][𝑦 / 𝑏](𝜑 ∧ 𝜓)))
20	13, 19	jca 514	. . . 4 ⊢ (∀𝑥∀𝑦(([𝑥 / 𝑎][𝑦 / 𝑏]𝜑 ↔ [𝑦 / 𝑎][𝑥 / 𝑏]𝜑) ∧ ([𝑥 / 𝑎][𝑦 / 𝑏]𝜓 ↔ [𝑦 / 𝑎][𝑥 / 𝑏]𝜓)) → (∀𝑥∀𝑦([𝑥 / 𝑎][𝑦 / 𝑏](𝜑 ∧ 𝜓) → [𝑦 / 𝑎][𝑥 / 𝑏](𝜑 ∧ 𝜓)) ∧ ∀𝑥∀𝑦([𝑦 / 𝑎][𝑥 / 𝑏](𝜑 ∧ 𝜓) → [𝑥 / 𝑎][𝑦 / 𝑏](𝜑 ∧ 𝜓))))
21	1, 20	sylbir 237	. . 3 ⊢ ((∀𝑥∀𝑦([𝑥 / 𝑎][𝑦 / 𝑏]𝜑 ↔ [𝑦 / 𝑎][𝑥 / 𝑏]𝜑) ∧ ∀𝑥∀𝑦([𝑥 / 𝑎][𝑦 / 𝑏]𝜓 ↔ [𝑦 / 𝑎][𝑥 / 𝑏]𝜓)) → (∀𝑥∀𝑦([𝑥 / 𝑎][𝑦 / 𝑏](𝜑 ∧ 𝜓) → [𝑦 / 𝑎][𝑥 / 𝑏](𝜑 ∧ 𝜓)) ∧ ∀𝑥∀𝑦([𝑦 / 𝑎][𝑥 / 𝑏](𝜑 ∧ 𝜓) → [𝑥 / 𝑎][𝑦 / 𝑏](𝜑 ∧ 𝜓))))
22		2albiim 1890	. . 3 ⊢ (∀𝑥∀𝑦([𝑥 / 𝑎][𝑦 / 𝑏](𝜑 ∧ 𝜓) ↔ [𝑦 / 𝑎][𝑥 / 𝑏](𝜑 ∧ 𝜓)) ↔ (∀𝑥∀𝑦([𝑥 / 𝑎][𝑦 / 𝑏](𝜑 ∧ 𝜓) → [𝑦 / 𝑎][𝑥 / 𝑏](𝜑 ∧ 𝜓)) ∧ ∀𝑥∀𝑦([𝑦 / 𝑎][𝑥 / 𝑏](𝜑 ∧ 𝜓) → [𝑥 / 𝑎][𝑦 / 𝑏](𝜑 ∧ 𝜓))))
23	21, 22	sylibr 236	. 2 ⊢ ((∀𝑥∀𝑦([𝑥 / 𝑎][𝑦 / 𝑏]𝜑 ↔ [𝑦 / 𝑎][𝑥 / 𝑏]𝜑) ∧ ∀𝑥∀𝑦([𝑥 / 𝑎][𝑦 / 𝑏]𝜓 ↔ [𝑦 / 𝑎][𝑥 / 𝑏]𝜓)) → ∀𝑥∀𝑦([𝑥 / 𝑎][𝑦 / 𝑏](𝜑 ∧ 𝜓) ↔ [𝑦 / 𝑎][𝑥 / 𝑏](𝜑 ∧ 𝜓)))
24		dfich2 43687	. . 3 ⊢ ([𝑎⇄𝑏]𝜑 ↔ ∀𝑥∀𝑦([𝑥 / 𝑎][𝑦 / 𝑏]𝜑 ↔ [𝑦 / 𝑎][𝑥 / 𝑏]𝜑))
25		dfich2 43687	. . 3 ⊢ ([𝑎⇄𝑏]𝜓 ↔ ∀𝑥∀𝑦([𝑥 / 𝑎][𝑦 / 𝑏]𝜓 ↔ [𝑦 / 𝑎][𝑥 / 𝑏]𝜓))
26	24, 25	anbi12i 628	. 2 ⊢ (([𝑎⇄𝑏]𝜑 ∧ [𝑎⇄𝑏]𝜓) ↔ (∀𝑥∀𝑦([𝑥 / 𝑎][𝑦 / 𝑏]𝜑 ↔ [𝑦 / 𝑎][𝑥 / 𝑏]𝜑) ∧ ∀𝑥∀𝑦([𝑥 / 𝑎][𝑦 / 𝑏]𝜓 ↔ [𝑦 / 𝑎][𝑥 / 𝑏]𝜓)))
27		dfich2 43687	. 2 ⊢ ([𝑎⇄𝑏](𝜑 ∧ 𝜓) ↔ ∀𝑥∀𝑦([𝑥 / 𝑎][𝑦 / 𝑏](𝜑 ∧ 𝜓) ↔ [𝑦 / 𝑎][𝑥 / 𝑏](𝜑 ∧ 𝜓)))
28	23, 26, 27	3imtr4i 294	1 ⊢ (([𝑎⇄𝑏]𝜑 ∧ [𝑎⇄𝑏]𝜓) → [𝑎⇄𝑏](𝜑 ∧ 𝜓))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398  ∀wal 1534  [wsb 2068  [wich 43679

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-10 2144  ax-11 2160  ax-12 2176

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-ich 43680

This theorem is referenced by: (None)