![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > sban | Structured version Visualization version GIF version |
Description: Conjunction inside and outside of a substitution are equivalent. (Contributed by NM, 14-May-1993.) |
Ref | Expression |
---|---|
sban | ⊢ ([𝑦 / 𝑥](𝜑 ∧ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sbn 2419 | . . 3 ⊢ ([𝑦 / 𝑥] ¬ (𝜑 → ¬ 𝜓) ↔ ¬ [𝑦 / 𝑥](𝜑 → ¬ 𝜓)) | |
2 | sbim 2423 | . . . 4 ⊢ ([𝑦 / 𝑥](𝜑 → ¬ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥] ¬ 𝜓)) | |
3 | sbn 2419 | . . . . 5 ⊢ ([𝑦 / 𝑥] ¬ 𝜓 ↔ ¬ [𝑦 / 𝑥]𝜓) | |
4 | 3 | imbi2i 325 | . . . 4 ⊢ (([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥] ¬ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 → ¬ [𝑦 / 𝑥]𝜓)) |
5 | 2, 4 | bitri 264 | . . 3 ⊢ ([𝑦 / 𝑥](𝜑 → ¬ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 → ¬ [𝑦 / 𝑥]𝜓)) |
6 | 1, 5 | xchbinx 323 | . 2 ⊢ ([𝑦 / 𝑥] ¬ (𝜑 → ¬ 𝜓) ↔ ¬ ([𝑦 / 𝑥]𝜑 → ¬ [𝑦 / 𝑥]𝜓)) |
7 | df-an 385 | . . 3 ⊢ ((𝜑 ∧ 𝜓) ↔ ¬ (𝜑 → ¬ 𝜓)) | |
8 | 7 | sbbii 1944 | . 2 ⊢ ([𝑦 / 𝑥](𝜑 ∧ 𝜓) ↔ [𝑦 / 𝑥] ¬ (𝜑 → ¬ 𝜓)) |
9 | df-an 385 | . 2 ⊢ (([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓) ↔ ¬ ([𝑦 / 𝑥]𝜑 → ¬ [𝑦 / 𝑥]𝜓)) | |
10 | 6, 8, 9 | 3bitr4i 292 | 1 ⊢ ([𝑦 / 𝑥](𝜑 ∧ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 196 ∧ wa 383 [wsb 1937 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-10 2059 ax-12 2087 ax-13 2282 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-ex 1745 df-nf 1750 df-sb 1938 |
This theorem is referenced by: sb3an 2428 sbbi 2429 sbabel 2822 cbvreu 3199 sbcan 3511 rmo3 3561 inab 3928 difab 3929 exss 4961 inopab 5285 mo5f 29452 rmo3f 29462 iuninc 29505 suppss2f 29567 fmptdF 29584 disjdsct 29608 esumpfinvalf 30266 measiuns 30408 ballotlemodife 30687 sb5ALT 39048 sbcangOLD 39056 2uasbanh 39094 2uasbanhVD 39461 sb5ALTVD 39463 ellimcabssub0 40167 |
Copyright terms: Public domain | W3C validator |