![]() |
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 1867. (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 2071 | . . 3 ⊢ ([𝑦 / 𝑥](𝜑 ∧ 𝜓) → [𝑦 / 𝑥]𝜑) |
3 | simpr 484 | . . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜓) | |
4 | 3 | sbimi 2071 | . . 3 ⊢ ([𝑦 / 𝑥](𝜑 ∧ 𝜓) → [𝑦 / 𝑥]𝜓) |
5 | 2, 4 | jca 511 | . 2 ⊢ ([𝑦 / 𝑥](𝜑 ∧ 𝜓) → ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓)) |
6 | pm3.2 469 | . . . 4 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓))) | |
7 | 6 | sb2imi 2072 | . . 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 2061 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 |
This theorem depends on definitions: df-bi 207 df-an 396 df-sb 2062 |
This theorem is referenced by: sb3an 2078 sbbi 2306 sbabel 2935 sbabelOLD 2936 cbvreuwOLD 3412 cbvreu 3424 rmo3f 3742 sbcan 3843 rmo3 3897 inab 4314 difab 4315 exss 5473 inopab 5841 difopab 5842 mo5f 32516 iuninc 32580 suppss2f 32654 fmptdF 32672 disjdsct 32717 esumpfinvalf 34056 measiuns 34197 ballotlemodife 34478 xpab 35705 sbn1ALT 36840 sb5ALT 44522 2uasbanh 44558 2uasbanhVD 44908 sb5ALTVD 44910 ellimcabssub0 45572 ichan 47379 |
Copyright terms: Public domain | W3C validator |