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 45266
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 45257 instead of dfich2 45269 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 2082 . . . . . . . 8 ([𝑥 / 𝑏](𝜑𝜓) ↔ ([𝑥 / 𝑏]𝜑 ∧ [𝑥 / 𝑏]𝜓))
21sbbii 2078 . . . . . . 7 ([𝑏 / 𝑎][𝑥 / 𝑏](𝜑𝜓) ↔ [𝑏 / 𝑎]([𝑥 / 𝑏]𝜑 ∧ [𝑥 / 𝑏]𝜓))
32sbbii 2078 . . . . . 6 ([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏](𝜑𝜓) ↔ [𝑎 / 𝑥][𝑏 / 𝑎]([𝑥 / 𝑏]𝜑 ∧ [𝑥 / 𝑏]𝜓))
4 sban 2082 . . . . . . 7 ([𝑏 / 𝑎]([𝑥 / 𝑏]𝜑 ∧ [𝑥 / 𝑏]𝜓) ↔ ([𝑏 / 𝑎][𝑥 / 𝑏]𝜑 ∧ [𝑏 / 𝑎][𝑥 / 𝑏]𝜓))
54sbbii 2078 . . . . . 6 ([𝑎 / 𝑥][𝑏 / 𝑎]([𝑥 / 𝑏]𝜑 ∧ [𝑥 / 𝑏]𝜓) ↔ [𝑎 / 𝑥]([𝑏 / 𝑎][𝑥 / 𝑏]𝜑 ∧ [𝑏 / 𝑎][𝑥 / 𝑏]𝜓))
6 sban 2082 . . . . . 6 ([𝑎 / 𝑥]([𝑏 / 𝑎][𝑥 / 𝑏]𝜑 ∧ [𝑏 / 𝑎][𝑥 / 𝑏]𝜓) ↔ ([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜑 ∧ [𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜓))
73, 5, 63bitri 296 . . . . 5 ([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏](𝜑𝜓) ↔ ([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜑 ∧ [𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜓))
8 pm4.38 635 . . . . 5 ((([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜑𝜑) ∧ ([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜓𝜓)) → (([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜑 ∧ [𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜓) ↔ (𝜑𝜓)))
97, 8bitrid 282 . . . 4 ((([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜑𝜑) ∧ ([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜓𝜓)) → ([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏](𝜑𝜓) ↔ (𝜑𝜓)))
109alanimi 1817 . . 3 ((∀𝑏([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜑𝜑) ∧ ∀𝑏([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜓𝜓)) → ∀𝑏([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏](𝜑𝜓) ↔ (𝜑𝜓)))
1110alanimi 1817 . 2 ((∀𝑎𝑏([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜑𝜑) ∧ ∀𝑎𝑏([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜓𝜓)) → ∀𝑎𝑏([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏](𝜑𝜓) ↔ (𝜑𝜓)))
12 df-ich 45257 . . 3 ([𝑎𝑏]𝜑 ↔ ∀𝑎𝑏([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜑𝜑))
13 df-ich 45257 . . 3 ([𝑎𝑏]𝜓 ↔ ∀𝑎𝑏([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜓𝜓))
1412, 13anbi12i 627 . 2 (([𝑎𝑏]𝜑 ∧ [𝑎𝑏]𝜓) ↔ (∀𝑎𝑏([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜑𝜑) ∧ ∀𝑎𝑏([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜓𝜓)))
15 df-ich 45257 . 2 ([𝑎𝑏](𝜑𝜓) ↔ ∀𝑎𝑏([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏](𝜑𝜓) ↔ (𝜑𝜓)))
1611, 14, 153imtr4i 291 1 (([𝑎𝑏]𝜑 ∧ [𝑎𝑏]𝜓) → [𝑎𝑏](𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  wal 1538  [wsb 2066  [wich 45256
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810
This theorem depends on definitions:  df-bi 206  df-an 397  df-sb 2067  df-ich 45257
This theorem is referenced by:  ichim  45268
  Copyright terms: Public domain W3C validator