Users' Mathboxes Mathbox for Alan Sare < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  sbcbi Structured version   Visualization version   GIF version

Theorem sbcbi 42183
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.)
Assertion
Ref Expression
sbcbi (𝐴𝑉 → (∀𝑥(𝜑𝜓) → ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓)))

Proof of Theorem sbcbi
StepHypRef Expression
1 spsbc 3731 . 2 (𝐴𝑉 → (∀𝑥(𝜑𝜓) → [𝐴 / 𝑥](𝜑𝜓)))
2 sbcbig 3772 . 2 (𝐴𝑉 → ([𝐴 / 𝑥](𝜑𝜓) ↔ ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓)))
31, 2sylibd 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