Metamath Proof Explorer

Theorem ichan

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)

Ref Expression
Assertion ichan ⊢ a ⇄ b φ ∧ a ⇄ b ψ → a ⇄ b φ ∧ ψ

Proof

Step Hyp Ref Expression
1 19.26-2 ⊢ ∀ x ∀ y x a y b φ ↔ y a x b φ ∧ x a y b ψ ↔ y a x b ψ ↔ ∀ x ∀ y x a y b φ ↔ y a x b φ ∧ ∀ x ∀ y x a y b ψ ↔ y a x b ψ
2 pm4.38 ⊢ x a y b φ ↔ y a x b φ ∧ x a y b ψ ↔ y a x b ψ → x a y b φ ∧ x a y b ψ ↔ y a x b φ ∧ y a x b ψ
3 2 biimpd ⊢ x a y b φ ↔ y a x b φ ∧ x a y b ψ ↔ y a x b ψ → x a y b φ ∧ x a y b ψ → y a x b φ ∧ y a x b ψ
4 sban ⊢ y b φ ∧ ψ ↔ y b φ ∧ y b ψ
5 4 sbbii ⊢ x a y b φ ∧ ψ ↔ x a y b φ ∧ y b ψ
6 sban ⊢ x a y b φ ∧ y b ψ ↔ x a y b φ ∧ x a y b ψ
7 5 6 bitri ⊢ x a y b φ ∧ ψ ↔ x a y b φ ∧ x a y b ψ
8 sban ⊢ x b φ ∧ ψ ↔ x b φ ∧ x b ψ
9 8 sbbii ⊢ y a x b φ ∧ ψ ↔ y a x b φ ∧ x b ψ
10 sban ⊢ y a x b φ ∧ x b ψ ↔ y a x b φ ∧ y a x b ψ
11 9 10 bitri ⊢ y a x b φ ∧ ψ ↔ y a x b φ ∧ y a x b ψ
12 3 7 11 3imtr4g ⊢ x a y b φ ↔ y a x b φ ∧ x a y b ψ ↔ y a x b ψ → x a y b φ ∧ ψ → y a x b φ ∧ ψ
13 12 2alimi ⊢ ∀ x ∀ y x a y b φ ↔ y a x b φ ∧ x a y b ψ ↔ y a x b ψ → ∀ x ∀ y x a y b φ ∧ ψ → y a x b φ ∧ ψ
14 bicom1 ⊢ x a y b φ ↔ y a x b φ → y a x b φ ↔ x a y b φ
15 bicom1 ⊢ x a y b ψ ↔ y a x b ψ → y a x b ψ ↔ x a y b ψ
16 14 15 bi2anan9 ⊢ x a y b φ ↔ y a x b φ ∧ x a y b ψ ↔ y a x b ψ → y a x b φ ∧ y a x b ψ ↔ x a y b φ ∧ x a y b ψ
17 16 biimpd ⊢ x a y b φ ↔ y a x b φ ∧ x a y b ψ ↔ y a x b ψ → y a x b φ ∧ y a x b ψ → x a y b φ ∧ x a y b ψ
18 17 11 7 3imtr4g ⊢ x a y b φ ↔ y a x b φ ∧ x a y b ψ ↔ y a x b ψ → y a x b φ ∧ ψ → x a y b φ ∧ ψ
19 18 2alimi ⊢ ∀ x ∀ y x a y b φ ↔ y a x b φ ∧ x a y b ψ ↔ y a x b ψ → ∀ x ∀ y y a x b φ ∧ ψ → x a y b φ ∧ ψ
20 13 19 jca ⊢ ∀ x ∀ y x a y b φ ↔ y a x b φ ∧ x a y b ψ ↔ y a x b ψ → ∀ x ∀ y x a y b φ ∧ ψ → y a x b φ ∧ ψ ∧ ∀ x ∀ y y a x b φ ∧ ψ → x a y b φ ∧ ψ
21 1 20 sylbir ⊢ ∀ x ∀ y x a y b φ ↔ y a x b φ ∧ ∀ x ∀ y x a y b ψ ↔ y a x b ψ → ∀ x ∀ y x a y b φ ∧ ψ → y a x b φ ∧ ψ ∧ ∀ x ∀ y y a x b φ ∧ ψ → x a y b φ ∧ ψ
22 2albiim ⊢ ∀ x ∀ y x a y b φ ∧ ψ ↔ y a x b φ ∧ ψ ↔ ∀ x ∀ y x a y b φ ∧ ψ → y a x b φ ∧ ψ ∧ ∀ x ∀ y y a x b φ ∧ ψ → x a y b φ ∧ ψ
23 21 22 sylibr ⊢ ∀ x ∀ y x a y b φ ↔ y a x b φ ∧ ∀ x ∀ y x a y b ψ ↔ y a x b ψ → ∀ x ∀ y x a y b φ ∧ ψ ↔ y a x b φ ∧ ψ
24 dfich2 ⊢ a ⇄ b φ ↔ ∀ x ∀ y x a y b φ ↔ y a x b φ
25 dfich2 ⊢ a ⇄ b ψ ↔ ∀ x ∀ y x a y b ψ ↔ y a x b ψ
26 24 25 anbi12i ⊢ a ⇄ b φ ∧ a ⇄ b ψ ↔ ∀ x ∀ y x a y b φ ↔ y a x b φ ∧ ∀ x ∀ y x a y b ψ ↔ y a x b ψ
27 dfich2 ⊢ a ⇄ b φ ∧ ψ ↔ ∀ x ∀ y x a y b φ ∧ ψ ↔ y a x b φ ∧ ψ
28 23 26 27 3imtr4i ⊢ a ⇄ b φ ∧ a ⇄ b ψ → a ⇄ b φ ∧ ψ