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) Use df-ich instead of dfich2 to reduce axioms. (Revised by SN, 4-May-2024)

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

Proof

Step Hyp Ref Expression
1 sban ⊢ ( [ 𝑥 / 𝑏 ] ( 𝜑 ∧ 𝜓 ) ↔ ( [ 𝑥 / 𝑏 ] 𝜑 ∧ [ 𝑥 / 𝑏 ] 𝜓 ) )
2 1 sbbii ⊢ ( [ 𝑏 / 𝑎 ] [ 𝑥 / 𝑏 ] ( 𝜑 ∧ 𝜓 ) ↔ [ 𝑏 / 𝑎 ] ( [ 𝑥 / 𝑏 ] 𝜑 ∧ [ 𝑥 / 𝑏 ] 𝜓 ) )
3 2 sbbii ⊢ ( [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑎 ] [ 𝑥 / 𝑏 ] ( 𝜑 ∧ 𝜓 ) ↔ [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑎 ] ( [ 𝑥 / 𝑏 ] 𝜑 ∧ [ 𝑥 / 𝑏 ] 𝜓 ) )
4 sban ⊢ ( [ 𝑏 / 𝑎 ] ( [ 𝑥 / 𝑏 ] 𝜑 ∧ [ 𝑥 / 𝑏 ] 𝜓 ) ↔ ( [ 𝑏 / 𝑎 ] [ 𝑥 / 𝑏 ] 𝜑 ∧ [ 𝑏 / 𝑎 ] [ 𝑥 / 𝑏 ] 𝜓 ) )
5 4 sbbii ⊢ ( [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑎 ] ( [ 𝑥 / 𝑏 ] 𝜑 ∧ [ 𝑥 / 𝑏 ] 𝜓 ) ↔ [ 𝑎 / 𝑥 ] ( [ 𝑏 / 𝑎 ] [ 𝑥 / 𝑏 ] 𝜑 ∧ [ 𝑏 / 𝑎 ] [ 𝑥 / 𝑏 ] 𝜓 ) )
6 sban ⊢ ( [ 𝑎 / 𝑥 ] ( [ 𝑏 / 𝑎 ] [ 𝑥 / 𝑏 ] 𝜑 ∧ [ 𝑏 / 𝑎 ] [ 𝑥 / 𝑏 ] 𝜓 ) ↔ ( [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑎 ] [ 𝑥 / 𝑏 ] 𝜑 ∧ [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑎 ] [ 𝑥 / 𝑏 ] 𝜓 ) )
7 3 5 6 3bitri ⊢ ( [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑎 ] [ 𝑥 / 𝑏 ] ( 𝜑 ∧ 𝜓 ) ↔ ( [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑎 ] [ 𝑥 / 𝑏 ] 𝜑 ∧ [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑎 ] [ 𝑥 / 𝑏 ] 𝜓 ) )
8 pm4.38 ⊢ ( ( ( [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑎 ] [ 𝑥 / 𝑏 ] 𝜑 ↔ 𝜑 ) ∧ ( [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑎 ] [ 𝑥 / 𝑏 ] 𝜓 ↔ 𝜓 ) ) → ( ( [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑎 ] [ 𝑥 / 𝑏 ] 𝜑 ∧ [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑎 ] [ 𝑥 / 𝑏 ] 𝜓 ) ↔ ( 𝜑 ∧ 𝜓 ) ) )
9 7 8 syl5bb ⊢ ( ( ( [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑎 ] [ 𝑥 / 𝑏 ] 𝜑 ↔ 𝜑 ) ∧ ( [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑎 ] [ 𝑥 / 𝑏 ] 𝜓 ↔ 𝜓 ) ) → ( [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑎 ] [ 𝑥 / 𝑏 ] ( 𝜑 ∧ 𝜓 ) ↔ ( 𝜑 ∧ 𝜓 ) ) )
10 9 alanimi ⊢ ( ( ∀ 𝑏 ( [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑎 ] [ 𝑥 / 𝑏 ] 𝜑 ↔ 𝜑 ) ∧ ∀ 𝑏 ( [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑎 ] [ 𝑥 / 𝑏 ] 𝜓 ↔ 𝜓 ) ) → ∀ 𝑏 ( [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑎 ] [ 𝑥 / 𝑏 ] ( 𝜑 ∧ 𝜓 ) ↔ ( 𝜑 ∧ 𝜓 ) ) )
11 10 alanimi ⊢ ( ( ∀ 𝑎 ∀ 𝑏 ( [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑎 ] [ 𝑥 / 𝑏 ] 𝜑 ↔ 𝜑 ) ∧ ∀ 𝑎 ∀ 𝑏 ( [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑎 ] [ 𝑥 / 𝑏 ] 𝜓 ↔ 𝜓 ) ) → ∀ 𝑎 ∀ 𝑏 ( [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑎 ] [ 𝑥 / 𝑏 ] ( 𝜑 ∧ 𝜓 ) ↔ ( 𝜑 ∧ 𝜓 ) ) )
12 df-ich ⊢ ( [ 𝑎 ⇄ 𝑏 ] 𝜑 ↔ ∀ 𝑎 ∀ 𝑏 ( [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑎 ] [ 𝑥 / 𝑏 ] 𝜑 ↔ 𝜑 ) )
13 df-ich ⊢ ( [ 𝑎 ⇄ 𝑏 ] 𝜓 ↔ ∀ 𝑎 ∀ 𝑏 ( [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑎 ] [ 𝑥 / 𝑏 ] 𝜓 ↔ 𝜓 ) )
14 12 13 anbi12i ⊢ ( ( [ 𝑎 ⇄ 𝑏 ] 𝜑 ∧ [ 𝑎 ⇄ 𝑏 ] 𝜓 ) ↔ ( ∀ 𝑎 ∀ 𝑏 ( [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑎 ] [ 𝑥 / 𝑏 ] 𝜑 ↔ 𝜑 ) ∧ ∀ 𝑎 ∀ 𝑏 ( [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑎 ] [ 𝑥 / 𝑏 ] 𝜓 ↔ 𝜓 ) ) )
15 df-ich ⊢ ( [ 𝑎 ⇄ 𝑏 ] ( 𝜑 ∧ 𝜓 ) ↔ ∀ 𝑎 ∀ 𝑏 ( [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑎 ] [ 𝑥 / 𝑏 ] ( 𝜑 ∧ 𝜓 ) ↔ ( 𝜑 ∧ 𝜓 ) ) )
16 11 14 15 3imtr4i ⊢ ( ( [ 𝑎 ⇄ 𝑏 ] 𝜑 ∧ [ 𝑎 ⇄ 𝑏 ] 𝜓 ) → [ 𝑎 ⇄ 𝑏 ] ( 𝜑 ∧ 𝜓 ) )