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 2391 | . . 3 ⊢ ([𝑦 / 𝑥] ¬ (𝜑 → ¬ 𝜓) ↔ ¬ [𝑦 / 𝑥](𝜑 → ¬ 𝜓)) | |
2 | sbim 2395 | . . . 4 ⊢ ([𝑦 / 𝑥](𝜑 → ¬ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥] ¬ 𝜓)) | |
3 | sbn 2391 | . . . . 5 ⊢ ([𝑦 / 𝑥] ¬ 𝜓 ↔ ¬ [𝑦 / 𝑥]𝜓) | |
4 | 3 | imbi2i 326 | . . . 4 ⊢ (([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥] ¬ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 → ¬ [𝑦 / 𝑥]𝜓)) |
5 | 2, 4 | bitri 264 | . . 3 ⊢ ([𝑦 / 𝑥](𝜑 → ¬ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 → ¬ [𝑦 / 𝑥]𝜓)) |
6 | 1, 5 | xchbinx 324 | . 2 ⊢ ([𝑦 / 𝑥] ¬ (𝜑 → ¬ 𝜓) ↔ ¬ ([𝑦 / 𝑥]𝜑 → ¬ [𝑦 / 𝑥]𝜓)) |
7 | df-an 386 | . . 3 ⊢ ((𝜑 ∧ 𝜓) ↔ ¬ (𝜑 → ¬ 𝜓)) | |
8 | 7 | sbbii 1887 | . 2 ⊢ ([𝑦 / 𝑥](𝜑 ∧ 𝜓) ↔ [𝑦 / 𝑥] ¬ (𝜑 → ¬ 𝜓)) |
9 | df-an 386 | . 2 ⊢ (([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓) ↔ ¬ ([𝑦 / 𝑥]𝜑 → ¬ [𝑦 / 𝑥]𝜓)) | |
10 | 6, 8, 9 | 3bitr4i 292 | 1 ⊢ ([𝑦 / 𝑥](𝜑 ∧ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 196 ∧ wa 384 [wsb 1880 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-10 2019 ax-12 2047 ax-13 2246 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-ex 1705 df-nf 1710 df-sb 1881 |
This theorem is referenced by: sb3an 2400 sbbi 2401 sbabel 2793 cbvreu 3169 sbcan 3478 rmo3 3528 inab 3895 difab 3896 exss 4931 inopab 5252 mo5f 29324 rmo3f 29335 iuninc 29379 suppss2f 29439 fmptdF 29456 disjdsct 29480 esumpfinvalf 30138 measiuns 30280 ballotlemodife 30559 sb5ALT 38731 sbcangOLD 38739 2uasbanh 38777 2uasbanhVD 39147 sb5ALTVD 39149 ellimcabssub0 39849 |
Copyright terms: Public domain | W3C validator |