Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ichan Structured version   Visualization version   GIF version

Theorem ichan 47380
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 47371 instead of dfich2 47383 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.
StepHypRef Expression
1 sban 2078 . . . . . . . 8 ([𝑥 / 𝑏](𝜑𝜓) ↔ ([𝑥 / 𝑏]𝜑 ∧ [𝑥 / 𝑏]𝜓))
21sbbii 2074 . . . . . . 7 ([𝑏 / 𝑎][𝑥 / 𝑏](𝜑𝜓) ↔ [𝑏 / 𝑎]([𝑥 / 𝑏]𝜑 ∧ [𝑥 / 𝑏]𝜓))
32sbbii 2074 . . . . . 6 ([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏](𝜑𝜓) ↔ [𝑎 / 𝑥][𝑏 / 𝑎]([𝑥 / 𝑏]𝜑 ∧ [𝑥 / 𝑏]𝜓))
4 sban 2078 . . . . . . 7 ([𝑏 / 𝑎]([𝑥 / 𝑏]𝜑 ∧ [𝑥 / 𝑏]𝜓) ↔ ([𝑏 / 𝑎][𝑥 / 𝑏]𝜑 ∧ [𝑏 / 𝑎][𝑥 / 𝑏]𝜓))
54sbbii 2074 . . . . . 6 ([𝑎 / 𝑥][𝑏 / 𝑎]([𝑥 / 𝑏]𝜑 ∧ [𝑥 / 𝑏]𝜓) ↔ [𝑎 / 𝑥]([𝑏 / 𝑎][𝑥 / 𝑏]𝜑 ∧ [𝑏 / 𝑎][𝑥 / 𝑏]𝜓))
6 sban 2078 . . . . . 6 ([𝑎 / 𝑥]([𝑏 / 𝑎][𝑥 / 𝑏]𝜑 ∧ [𝑏 / 𝑎][𝑥 / 𝑏]𝜓) ↔ ([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜑 ∧ [𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜓))
73, 5, 63bitri 297 . . . . 5 ([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏](𝜑𝜓) ↔ ([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜑 ∧ [𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜓))
8 pm4.38 637 . . . . 5 ((([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜑𝜑) ∧ ([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜓𝜓)) → (([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜑 ∧ [𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜓) ↔ (𝜑𝜓)))
97, 8bitrid 283 . . . 4 ((([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜑𝜑) ∧ ([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜓𝜓)) → ([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏](𝜑𝜓) ↔ (𝜑𝜓)))
109alanimi 1813 . . 3 ((∀𝑏([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜑𝜑) ∧ ∀𝑏([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜓𝜓)) → ∀𝑏([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏](𝜑𝜓) ↔ (𝜑𝜓)))
1110alanimi 1813 . 2 ((∀𝑎𝑏([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜑𝜑) ∧ ∀𝑎𝑏([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜓𝜓)) → ∀𝑎𝑏([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏](𝜑𝜓) ↔ (𝜑𝜓)))
12 df-ich 47371 . . 3 ([𝑎𝑏]𝜑 ↔ ∀𝑎𝑏([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜑𝜑))
13 df-ich 47371 . . 3 ([𝑎𝑏]𝜓 ↔ ∀𝑎𝑏([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜓𝜓))
1412, 13anbi12i 628 . 2 (([𝑎𝑏]𝜑 ∧ [𝑎𝑏]𝜓) ↔ (∀𝑎𝑏([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜑𝜑) ∧ ∀𝑎𝑏([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜓𝜓)))
15 df-ich 47371 . 2 ([𝑎𝑏](𝜑𝜓) ↔ ∀𝑎𝑏([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏](𝜑𝜓) ↔ (𝜑𝜓)))
1611, 14, 153imtr4i 292 1 (([𝑎𝑏]𝜑 ∧ [𝑎𝑏]𝜓) → [𝑎𝑏](𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  wal 1535  [wsb 2062  [wich 47370
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806
This theorem depends on definitions:  df-bi 207  df-an 396  df-sb 2063  df-ich 47371
This theorem is referenced by:  ichim  47382
  Copyright terms: Public domain W3C validator