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 485 | . . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜑) | |
2 | 1 | sbimi 2079 | . . 3 ⊢ ([𝑦 / 𝑥](𝜑 ∧ 𝜓) → [𝑦 / 𝑥]𝜑) |
3 | simpr 487 | . . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜓) | |
4 | 3 | sbimi 2079 | . . 3 ⊢ ([𝑦 / 𝑥](𝜑 ∧ 𝜓) → [𝑦 / 𝑥]𝜓) |
5 | 2, 4 | jca 514 | . 2 ⊢ ([𝑦 / 𝑥](𝜑 ∧ 𝜓) → ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓)) |
6 | pm3.2 472 | . . . 4 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓))) | |
7 | 6 | sb2imi 2080 | . . 3 ⊢ ([𝑦 / 𝑥]𝜑 → ([𝑦 / 𝑥]𝜓 → [𝑦 / 𝑥](𝜑 ∧ 𝜓))) |
8 | 7 | imp 409 | . 2 ⊢ (([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓) → [𝑦 / 𝑥](𝜑 ∧ 𝜓)) |
9 | 5, 8 | impbii 211 | 1 ⊢ ([𝑦 / 𝑥](𝜑 ∧ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 208 ∧ wa 398 [wsb 2069 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 |
This theorem depends on definitions: df-bi 209 df-an 399 df-sb 2070 |
This theorem is referenced by: sb3an 2087 sbbi 2317 sbabel 3015 cbvreuw 3443 cbvreu 3447 rmo3f 3725 sbcan 3821 rmo3 3872 rmo3OLD 3873 inab 4271 difab 4272 exss 5355 inopab 5701 mo5f 30253 iuninc 30312 suppss2f 30384 fmptdF 30401 disjdsct 30438 esumpfinvalf 31335 measiuns 31476 ballotlemodife 31755 wl-dfrabv 34877 wl-dfrabf 34879 sb5ALT 40879 2uasbanh 40915 2uasbanhVD 41265 sb5ALTVD 41267 ellimcabssub0 41918 ichan 43650 |
Copyright terms: Public domain | W3C validator |