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 3778. sbcbi 42183 is sbcbiVD 42520 without virtual deductions and was automatically derived from sbcbiVD 42520 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 3731 | . 2 ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝜑 ↔ 𝜓) → [𝐴 / 𝑥](𝜑 ↔ 𝜓))) | |
2 | sbcbig 3772 | . 2 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥](𝜑 ↔ 𝜓) ↔ ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓))) | |
3 | 1, 2 | sylibd 238 | 1 ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝜑 ↔ 𝜓) → ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∀wal 1535 ∈ wcel 2101 [wsbc 3718 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2103 ax-9 2111 ax-10 2132 ax-12 2166 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-tru 1540 df-ex 1778 df-nf 1782 df-sb 2063 df-clab 2711 df-cleq 2725 df-clel 2811 df-sbc 3719 |
This theorem is referenced by: trsbcVD 42521 sbcssgVD 42527 |
Copyright terms: Public domain | W3C validator |