![]() |
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. Compare 19.26 1871. (Contributed by NM, 14-May-1993.) (Proof shortened by Steven Nguyen, 13-Aug-2023.) |
Ref | Expression |
---|---|
sban | ⊢ ([𝑦 / 𝑥](𝜑 ∧ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl 486 | . . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜑) | |
2 | 1 | sbimi 2079 | . . 3 ⊢ ([𝑦 / 𝑥](𝜑 ∧ 𝜓) → [𝑦 / 𝑥]𝜑) |
3 | simpr 488 | . . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜓) | |
4 | 3 | sbimi 2079 | . . 3 ⊢ ([𝑦 / 𝑥](𝜑 ∧ 𝜓) → [𝑦 / 𝑥]𝜓) |
5 | 2, 4 | jca 515 | . 2 ⊢ ([𝑦 / 𝑥](𝜑 ∧ 𝜓) → ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓)) |
6 | pm3.2 473 | . . . 4 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓))) | |
7 | 6 | sb2imi 2080 | . . 3 ⊢ ([𝑦 / 𝑥]𝜑 → ([𝑦 / 𝑥]𝜓 → [𝑦 / 𝑥](𝜑 ∧ 𝜓))) |
8 | 7 | imp 410 | . 2 ⊢ (([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓) → [𝑦 / 𝑥](𝜑 ∧ 𝜓)) |
9 | 5, 8 | impbii 212 | 1 ⊢ ([𝑦 / 𝑥](𝜑 ∧ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 209 ∧ wa 399 [wsb 2069 |
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 |
This theorem is referenced by: sb3an 2086 sbbi 2313 sbabel 2986 cbvreuw 3389 cbvreu 3394 rmo3f 3673 sbcan 3768 rmo3 3818 inab 4223 difab 4224 exss 5320 inopab 5665 mo5f 30260 iuninc 30324 suppss2f 30398 fmptdF 30419 disjdsct 30462 esumpfinvalf 31445 measiuns 31586 ballotlemodife 31865 wl-dfrabv 35027 wl-dfrabf 35029 sb5ALT 41231 2uasbanh 41267 2uasbanhVD 41617 sb5ALTVD 41619 ellimcabssub0 42259 ichan 43972 |
Copyright terms: Public domain | W3C validator |