![]() |
Mathbox for Alan Sare |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > sbcim2g | Structured version Visualization version GIF version |
Description: Distribution of class substitution over a left-nested implication. Similar to sbcimg 3821. sbcim2g 43813 is sbcim2gVD 44150 without virtual deductions and was automatically derived from sbcim2gVD 44150 using the tools program translate..without..overwriting.cmd and Metamath's minimize command. (Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.) |
Ref | Expression |
---|---|
sbcim2g | ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥](𝜑 → (𝜓 → 𝜒)) ↔ ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒)))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sbcimg 3821 | . . . 4 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥](𝜑 → (𝜓 → 𝜒)) ↔ ([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥](𝜓 → 𝜒)))) | |
2 | 1 | biimpd 228 | . . 3 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥](𝜑 → (𝜓 → 𝜒)) → ([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥](𝜓 → 𝜒)))) |
3 | sbcimg 3821 | . . 3 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥](𝜓 → 𝜒) ↔ ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒))) | |
4 | imbi2 348 | . . . 4 ⊢ (([𝐴 / 𝑥](𝜓 → 𝜒) ↔ ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒)) → (([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥](𝜓 → 𝜒)) ↔ ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒)))) | |
5 | 4 | biimpcd 248 | . . 3 ⊢ (([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥](𝜓 → 𝜒)) → (([𝐴 / 𝑥](𝜓 → 𝜒) ↔ ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒)) → ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒)))) |
6 | 2, 3, 5 | syl6ci 71 | . 2 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥](𝜑 → (𝜓 → 𝜒)) → ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒)))) |
7 | idd 24 | . . . 4 ⊢ (𝐴 ∈ 𝑉 → (([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒)) → ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒)))) | |
8 | biimpr 219 | . . . 4 ⊢ (([𝐴 / 𝑥](𝜓 → 𝜒) ↔ ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒)) → (([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒) → [𝐴 / 𝑥](𝜓 → 𝜒))) | |
9 | 3, 7, 8 | ee13 43779 | . . 3 ⊢ (𝐴 ∈ 𝑉 → (([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒)) → ([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥](𝜓 → 𝜒)))) |
10 | 9, 1 | sylibrd 259 | . 2 ⊢ (𝐴 ∈ 𝑉 → (([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒)) → [𝐴 / 𝑥](𝜑 → (𝜓 → 𝜒)))) |
11 | 6, 10 | impbid 211 | 1 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥](𝜑 → (𝜓 → 𝜒)) ↔ ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒)))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∈ wcel 2098 [wsbc 3770 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-12 2163 ax-ext 2695 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-tru 1536 df-ex 1774 df-nf 1778 df-sb 2060 df-clab 2702 df-cleq 2716 df-clel 2802 df-sbc 3771 |
This theorem is referenced by: trsbc 43815 trsbcVD 44152 |
Copyright terms: Public domain | W3C validator |