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 1873. (Contributed by NM, 14-May-1993.) (Proof shortened by Steven Nguyen, 13-Aug-2023.) |
Ref | Expression |
---|---|
sban | ⊢ ([𝑦 / 𝑥](𝜑 ∧ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl 483 | . . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜑) | |
2 | 1 | sbimi 2077 | . . 3 ⊢ ([𝑦 / 𝑥](𝜑 ∧ 𝜓) → [𝑦 / 𝑥]𝜑) |
3 | simpr 485 | . . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜓) | |
4 | 3 | sbimi 2077 | . . 3 ⊢ ([𝑦 / 𝑥](𝜑 ∧ 𝜓) → [𝑦 / 𝑥]𝜓) |
5 | 2, 4 | jca 512 | . 2 ⊢ ([𝑦 / 𝑥](𝜑 ∧ 𝜓) → ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓)) |
6 | pm3.2 470 | . . . 4 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓))) | |
7 | 6 | sb2imi 2078 | . . 3 ⊢ ([𝑦 / 𝑥]𝜑 → ([𝑦 / 𝑥]𝜓 → [𝑦 / 𝑥](𝜑 ∧ 𝜓))) |
8 | 7 | imp 407 | . 2 ⊢ (([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓) → [𝑦 / 𝑥](𝜑 ∧ 𝜓)) |
9 | 5, 8 | impbii 208 | 1 ⊢ ([𝑦 / 𝑥](𝜑 ∧ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∧ wa 396 [wsb 2067 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 |
This theorem depends on definitions: df-bi 206 df-an 397 df-sb 2068 |
This theorem is referenced by: sb3an 2084 sbbi 2305 sbabel 2941 sbabelOLD 2942 cbvreuwOLD 3377 cbvreu 3381 rmo3f 3669 sbcan 3768 rmo3 3822 inab 4233 difab 4234 exss 5378 inopab 5739 mo5f 30837 iuninc 30900 suppss2f 30974 fmptdF 30993 disjdsct 31035 esumpfinvalf 32044 measiuns 32185 ballotlemodife 32464 xpab 33677 sbn1ALT 35042 sb5ALT 42145 2uasbanh 42181 2uasbanhVD 42531 sb5ALTVD 42533 ellimcabssub0 43158 ichan 44907 |
Copyright terms: Public domain | W3C validator |