Mathbox for Alan Sare |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > sbcbi | Structured version Visualization version GIF version |
Description: Implication form of sbcbii 3781. sbcbi 42129 is sbcbiVD 42466 without virtual deductions and was automatically derived from sbcbiVD 42466 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 |
---|---|
sbcbi | ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝜑 ↔ 𝜓) → ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | spsbc 3733 | . 2 ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝜑 ↔ 𝜓) → [𝐴 / 𝑥](𝜑 ↔ 𝜓))) | |
2 | sbcbig 3774 | . 2 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥](𝜑 ↔ 𝜓) ↔ ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓))) | |
3 | 1, 2 | sylibd 238 | 1 ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝜑 ↔ 𝜓) → ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∀wal 1540 ∈ wcel 2110 [wsbc 3720 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2015 ax-8 2112 ax-9 2120 ax-10 2141 ax-12 2175 ax-ext 2711 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-tru 1545 df-ex 1787 df-nf 1791 df-sb 2072 df-clab 2718 df-cleq 2732 df-clel 2818 df-sbc 3721 |
This theorem is referenced by: trsbcVD 42467 sbcssgVD 42473 |
Copyright terms: Public domain | W3C validator |