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 44125
Description: Implication form of sbcbii 3834. sbcbi 44125 is sbcbiVD 44462 without virtual deductions and was automatically derived from sbcbiVD 44462 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 3786 . 2 (𝐴𝑉 → (∀𝑥(𝜑𝜓) → [𝐴 / 𝑥](𝜑𝜓)))
2 sbcbig 3828 . 2 (𝐴𝑉 → ([𝐴 / 𝑥](𝜑𝜓) ↔ ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓)))
31, 2sylibd 238 1 (𝐴𝑉 → (∀𝑥(𝜑𝜓) → ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wal 1531  wcel 2098  [wsbc 3773
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 2166  ax-ext 2696
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-tru 1536  df-ex 1774  df-nf 1778  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-sbc 3774
This theorem is referenced by:  trsbcVD  44463  sbcssgVD  44469
  Copyright terms: Public domain W3C validator