![]() |
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 1865. (Contributed by NM, 14-May-1993.) (Proof shortened by Steven Nguyen, 13-Aug-2023.) |
Ref | Expression |
---|---|
sban | ⊢ ([𝑦 / 𝑥](𝜑 ∧ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl 482 | . . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜑) | |
2 | 1 | sbimi 2069 | . . 3 ⊢ ([𝑦 / 𝑥](𝜑 ∧ 𝜓) → [𝑦 / 𝑥]𝜑) |
3 | simpr 484 | . . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜓) | |
4 | 3 | sbimi 2069 | . . 3 ⊢ ([𝑦 / 𝑥](𝜑 ∧ 𝜓) → [𝑦 / 𝑥]𝜓) |
5 | 2, 4 | jca 511 | . 2 ⊢ ([𝑦 / 𝑥](𝜑 ∧ 𝜓) → ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓)) |
6 | pm3.2 469 | . . . 4 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓))) | |
7 | 6 | sb2imi 2070 | . . 3 ⊢ ([𝑦 / 𝑥]𝜑 → ([𝑦 / 𝑥]𝜓 → [𝑦 / 𝑥](𝜑 ∧ 𝜓))) |
8 | 7 | imp 406 | . 2 ⊢ (([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓) → [𝑦 / 𝑥](𝜑 ∧ 𝜓)) |
9 | 5, 8 | impbii 208 | 1 ⊢ ([𝑦 / 𝑥](𝜑 ∧ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∧ wa 395 [wsb 2059 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 |
This theorem depends on definitions: df-bi 206 df-an 396 df-sb 2060 |
This theorem is referenced by: sb3an 2076 sbbi 2296 sbabel 2932 sbabelOLD 2933 cbvreuwOLD 3406 cbvreu 3418 rmo3f 3725 sbcan 3824 rmo3 3878 inab 4294 difab 4295 exss 5456 inopab 5822 difopab 5823 mo5f 32238 iuninc 32301 suppss2f 32372 fmptdF 32390 disjdsct 32431 esumpfinvalf 33604 measiuns 33745 ballotlemodife 34026 xpab 35229 sbn1ALT 36244 sb5ALT 43867 2uasbanh 43903 2uasbanhVD 44253 sb5ALTVD 44255 ellimcabssub0 44910 ichan 46700 |
Copyright terms: Public domain | W3C validator |