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 43959
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 43950 instead of dfich2 43962 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 2085 . . . . . . . 8 ([𝑥 / 𝑏](𝜑𝜓) ↔ ([𝑥 / 𝑏]𝜑 ∧ [𝑥 / 𝑏]𝜓))
21sbbii 2081 . . . . . . 7 ([𝑏 / 𝑎][𝑥 / 𝑏](𝜑𝜓) ↔ [𝑏 / 𝑎]([𝑥 / 𝑏]𝜑 ∧ [𝑥 / 𝑏]𝜓))
32sbbii 2081 . . . . . 6 ([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏](𝜑𝜓) ↔ [𝑎 / 𝑥][𝑏 / 𝑎]([𝑥 / 𝑏]𝜑 ∧ [𝑥 / 𝑏]𝜓))
4 sban 2085 . . . . . . 7 ([𝑏 / 𝑎]([𝑥 / 𝑏]𝜑 ∧ [𝑥 / 𝑏]𝜓) ↔ ([𝑏 / 𝑎][𝑥 / 𝑏]𝜑 ∧ [𝑏 / 𝑎][𝑥 / 𝑏]𝜓))
54sbbii 2081 . . . . . 6 ([𝑎 / 𝑥][𝑏 / 𝑎]([𝑥 / 𝑏]𝜑 ∧ [𝑥 / 𝑏]𝜓) ↔ [𝑎 / 𝑥]([𝑏 / 𝑎][𝑥 / 𝑏]𝜑 ∧ [𝑏 / 𝑎][𝑥 / 𝑏]𝜓))
6 sban 2085 . . . . . 6 ([𝑎 / 𝑥]([𝑏 / 𝑎][𝑥 / 𝑏]𝜑 ∧ [𝑏 / 𝑎][𝑥 / 𝑏]𝜓) ↔ ([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜑 ∧ [𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜓))
73, 5, 63bitri 300 . . . . 5 ([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏](𝜑𝜓) ↔ ([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜑 ∧ [𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜓))
8 pm4.38 637 . . . . 5 ((([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜑𝜑) ∧ ([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜓𝜓)) → (([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜑 ∧ [𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜓) ↔ (𝜑𝜓)))
97, 8syl5bb 286 . . . 4 ((([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜑𝜑) ∧ ([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜓𝜓)) → ([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏](𝜑𝜓) ↔ (𝜑𝜓)))
109alanimi 1818 . . 3 ((∀𝑏([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜑𝜑) ∧ ∀𝑏([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜓𝜓)) → ∀𝑏([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏](𝜑𝜓) ↔ (𝜑𝜓)))
1110alanimi 1818 . 2 ((∀𝑎𝑏([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜑𝜑) ∧ ∀𝑎𝑏([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜓𝜓)) → ∀𝑎𝑏([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏](𝜑𝜓) ↔ (𝜑𝜓)))
12 df-ich 43950 . . 3 ([𝑎𝑏]𝜑 ↔ ∀𝑎𝑏([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜑𝜑))
13 df-ich 43950 . . 3 ([𝑎𝑏]𝜓 ↔ ∀𝑎𝑏([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜓𝜓))
1412, 13anbi12i 629 . 2 (([𝑎𝑏]𝜑 ∧ [𝑎𝑏]𝜓) ↔ (∀𝑎𝑏([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜑𝜑) ∧ ∀𝑎𝑏([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏]𝜓𝜓)))
15 df-ich 43950 . 2 ([𝑎𝑏](𝜑𝜓) ↔ ∀𝑎𝑏([𝑎 / 𝑥][𝑏 / 𝑎][𝑥 / 𝑏](𝜑𝜓) ↔ (𝜑𝜓)))
1611, 14, 153imtr4i 295 1 (([𝑎𝑏]𝜑 ∧ [𝑎𝑏]𝜓) → [𝑎𝑏](𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  wal 1536  [wsb 2069  [wich 43949
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811
This theorem depends on definitions:  df-bi 210  df-an 400  df-sb 2070  df-ich 43950
This theorem is referenced by:  ichim  43961
  Copyright terms: Public domain W3C validator