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 47442
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 47433 instead of dfich2 47445 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 2080 . . . . . . . 8 ([𝑥 / 𝑏](𝜑𝜓) ↔ ([𝑥 / 𝑏]𝜑 ∧ [𝑥 / 𝑏]𝜓))
21sbbii 2076 . . . . . . 7 ([𝑏 / 𝑎][𝑥 / 𝑏](𝜑𝜓) ↔ [𝑏 / 𝑎]([𝑥 / 𝑏]𝜑 ∧ [𝑥 / 𝑏]𝜓))
32sbbii 2076 . . . . . 6 ([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏](𝜑𝜓) ↔ [𝑎 / 𝑥][𝑏 / 𝑎]([𝑥 / 𝑏]𝜑 ∧ [𝑥 / 𝑏]𝜓))
4 sban 2080 . . . . . . 7 ([𝑏 / 𝑎]([𝑥 / 𝑏]𝜑 ∧ [𝑥 / 𝑏]𝜓) ↔ ([𝑏 / 𝑎][𝑥 / 𝑏]𝜑 ∧ [𝑏 / 𝑎][𝑥 / 𝑏]𝜓))
54sbbii 2076 . . . . . 6 ([𝑎 / 𝑥][𝑏 / 𝑎]([𝑥 / 𝑏]𝜑 ∧ [𝑥 / 𝑏]𝜓) ↔ [𝑎 / 𝑥]([𝑏 / 𝑎][𝑥 / 𝑏]𝜑 ∧ [𝑏 / 𝑎][𝑥 / 𝑏]𝜓))
6 sban 2080 . . . . . 6 ([𝑎 / 𝑥]([𝑏 / 𝑎][𝑥 / 𝑏]𝜑 ∧ [𝑏 / 𝑎][𝑥 / 𝑏]𝜓) ↔ ([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜑 ∧ [𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜓))
73, 5, 63bitri 297 . . . . 5 ([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏](𝜑𝜓) ↔ ([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜑 ∧ [𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜓))
8 pm4.38 637 . . . . 5 ((([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜑𝜑) ∧ ([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜓𝜓)) → (([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜑 ∧ [𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜓) ↔ (𝜑𝜓)))
97, 8bitrid 283 . . . 4 ((([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜑𝜑) ∧ ([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜓𝜓)) → ([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏](𝜑𝜓) ↔ (𝜑𝜓)))
109alanimi 1816 . . 3 ((∀𝑏([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜑𝜑) ∧ ∀𝑏([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜓𝜓)) → ∀𝑏([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏](𝜑𝜓) ↔ (𝜑𝜓)))
1110alanimi 1816 . 2 ((∀𝑎𝑏([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜑𝜑) ∧ ∀𝑎𝑏([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜓𝜓)) → ∀𝑎𝑏([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏](𝜑𝜓) ↔ (𝜑𝜓)))
12 df-ich 47433 . . 3 ([𝑎𝑏]𝜑 ↔ ∀𝑎𝑏([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜑𝜑))
13 df-ich 47433 . . 3 ([𝑎𝑏]𝜓 ↔ ∀𝑎𝑏([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜓𝜓))
1412, 13anbi12i 628 . 2 (([𝑎𝑏]𝜑 ∧ [𝑎𝑏]𝜓) ↔ (∀𝑎𝑏([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜑𝜑) ∧ ∀𝑎𝑏([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜓𝜓)))
15 df-ich 47433 . 2 ([𝑎𝑏](𝜑𝜓) ↔ ∀𝑎𝑏([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏](𝜑𝜓) ↔ (𝜑𝜓)))
1611, 14, 153imtr4i 292 1 (([𝑎𝑏]𝜑 ∧ [𝑎𝑏]𝜓) → [𝑎𝑏](𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  wal 1538  [wsb 2064  [wich 47432
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809
This theorem depends on definitions:  df-bi 207  df-an 396  df-sb 2065  df-ich 47433
This theorem is referenced by:  ichim  47444
  Copyright terms: Public domain W3C validator