| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > sbc3an | GIF version | ||
| Description: Distribution of class substitution over triple conjunction. (Contributed by NM, 14-Dec-2006.) (Revised by NM, 17-Aug-2018.) |
| Ref | Expression |
|---|---|
| sbc3an | ⊢ ([𝐴 / 𝑥](𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ([𝐴 / 𝑥]𝜑 ∧ [𝐴 / 𝑥]𝜓 ∧ [𝐴 / 𝑥]𝜒)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-3an 1006 | . . . 4 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒)) | |
| 2 | 1 | sbcbii 3091 | . . 3 ⊢ ([𝐴 / 𝑥](𝜑 ∧ 𝜓 ∧ 𝜒) ↔ [𝐴 / 𝑥]((𝜑 ∧ 𝜓) ∧ 𝜒)) |
| 3 | sbcan 3074 | . . 3 ⊢ ([𝐴 / 𝑥]((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ ([𝐴 / 𝑥](𝜑 ∧ 𝜓) ∧ [𝐴 / 𝑥]𝜒)) | |
| 4 | sbcan 3074 | . . . 4 ⊢ ([𝐴 / 𝑥](𝜑 ∧ 𝜓) ↔ ([𝐴 / 𝑥]𝜑 ∧ [𝐴 / 𝑥]𝜓)) | |
| 5 | 4 | anbi1i 458 | . . 3 ⊢ (([𝐴 / 𝑥](𝜑 ∧ 𝜓) ∧ [𝐴 / 𝑥]𝜒) ↔ (([𝐴 / 𝑥]𝜑 ∧ [𝐴 / 𝑥]𝜓) ∧ [𝐴 / 𝑥]𝜒)) |
| 6 | 2, 3, 5 | 3bitri 206 | . 2 ⊢ ([𝐴 / 𝑥](𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (([𝐴 / 𝑥]𝜑 ∧ [𝐴 / 𝑥]𝜓) ∧ [𝐴 / 𝑥]𝜒)) |
| 7 | df-3an 1006 | . 2 ⊢ (([𝐴 / 𝑥]𝜑 ∧ [𝐴 / 𝑥]𝜓 ∧ [𝐴 / 𝑥]𝜒) ↔ (([𝐴 / 𝑥]𝜑 ∧ [𝐴 / 𝑥]𝜓) ∧ [𝐴 / 𝑥]𝜒)) | |
| 8 | 6, 7 | bitr4i 187 | 1 ⊢ ([𝐴 / 𝑥](𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ([𝐴 / 𝑥]𝜑 ∧ [𝐴 / 𝑥]𝜓 ∧ [𝐴 / 𝑥]𝜒)) |
| Colors of variables: wff set class |
| Syntax hints: ∧ wa 104 ↔ wb 105 ∧ w3a 1004 [wsbc 3031 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 716 ax-5 1495 ax-7 1496 ax-gen 1497 ax-ie1 1541 ax-ie2 1542 ax-8 1552 ax-10 1553 ax-11 1554 ax-i12 1555 ax-bndl 1557 ax-4 1558 ax-17 1574 ax-i9 1578 ax-ial 1582 ax-i5r 1583 ax-ext 2213 |
| This theorem depends on definitions: df-bi 117 df-3an 1006 df-tru 1400 df-nf 1509 df-sb 1811 df-clab 2218 df-cleq 2224 df-clel 2227 df-nfc 2363 df-v 2804 df-sbc 3032 |
| This theorem is referenced by: (None) |
| Copyright terms: Public domain | W3C validator |