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 41832
Description: Implication form of sbcbii 3755. sbcbi 41832 is sbcbiVD 42169 without virtual deductions and was automatically derived from sbcbiVD 42169 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 3707 . 2 (𝐴𝑉 → (∀𝑥(𝜑𝜓) → [𝐴 / 𝑥](𝜑𝜓)))
2 sbcbig 3748 . 2 (𝐴𝑉 → ([𝐴 / 𝑥](𝜑𝜓) ↔ ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓)))
31, 2sylibd 242 1 (𝐴𝑉 → (∀𝑥(𝜑𝜓) → ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wal 1541  wcel 2110  [wsbc 3694
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-12 2175  ax-ext 2708
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-tru 1546  df-ex 1788  df-nf 1792  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-sbc 3695
This theorem is referenced by:  trsbcVD  42170  sbcssgVD  42176
  Copyright terms: Public domain W3C validator