| 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 1870. (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 2074 | . . 3 ⊢ ([𝑦 / 𝑥](𝜑 ∧ 𝜓) → [𝑦 / 𝑥]𝜑) |
| 3 | simpr 484 | . . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜓) | |
| 4 | 3 | sbimi 2074 | . . 3 ⊢ ([𝑦 / 𝑥](𝜑 ∧ 𝜓) → [𝑦 / 𝑥]𝜓) |
| 5 | 2, 4 | jca 511 | . 2 ⊢ ([𝑦 / 𝑥](𝜑 ∧ 𝜓) → ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓)) |
| 6 | pm3.2 469 | . . . 4 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓))) | |
| 7 | 6 | sb2imi 2075 | . . 3 ⊢ ([𝑦 / 𝑥]𝜑 → ([𝑦 / 𝑥]𝜓 → [𝑦 / 𝑥](𝜑 ∧ 𝜓))) |
| 8 | 7 | imp 406 | . 2 ⊢ (([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓) → [𝑦 / 𝑥](𝜑 ∧ 𝜓)) |
| 9 | 5, 8 | impbii 209 | 1 ⊢ ([𝑦 / 𝑥](𝜑 ∧ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓)) |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 206 ∧ wa 395 [wsb 2064 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-sb 2065 |
| This theorem is referenced by: sb3an 2081 sbbi 2308 sbabel 2938 sbabelOLD 2939 cbvreuwOLD 3415 cbvreu 3428 rmo3f 3740 sbcan 3838 rmo3 3889 inab 4309 difab 4310 exss 5468 inopab 5839 difopab 5840 mo5f 32508 iuninc 32573 suppss2f 32648 fmptdF 32666 disjdsct 32712 esumpfinvalf 34077 measiuns 34218 ballotlemodife 34500 xpab 35726 sbn1ALT 36859 sb5ALT 44545 2uasbanh 44581 2uasbanhVD 44931 sb5ALTVD 44933 ellimcabssub0 45632 ichan 47442 |
| Copyright terms: Public domain | W3C validator |