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

Theorem sbcbiVD 44896
Description: Implication form of sbcbii 3846. The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. sbcbi 44559 is sbcbiVD 44896 without virtual deductions and was automatically derived from sbcbiVD 44896.
1:: (   𝐴𝐵   ▶   𝐴𝐵   )
2:: (   𝐴𝐵   ,   𝑥(𝜑𝜓)    ▶   𝑥(𝜑𝜓)   )
3:1,2: (   𝐴𝐵   ,   𝑥(𝜑𝜓)    ▶   [𝐴 / 𝑥](𝜑𝜓)   )
4:1,3: (   𝐴𝐵   ,   𝑥(𝜑𝜓)    ▶   ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓)   )
5:4: (   𝐴𝐵   ▶   (∀𝑥(𝜑𝜓) → ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓))   )
qed:5: (𝐴𝐵 → (∀𝑥(𝜑𝜓) → ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓)))
(Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
sbcbiVD (𝐴𝐵 → (∀𝑥(𝜑𝜓) → ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓)))

Proof of Theorem sbcbiVD
StepHypRef Expression
1 idn1 44594 . . . 4 (   𝐴𝐵   ▶   𝐴𝐵   )
2 idn2 44633 . . . . 5 (   𝐴𝐵   ,   𝑥(𝜑𝜓)   ▶   𝑥(𝜑𝜓)   )
3 spsbc 3801 . . . . 5 (𝐴𝐵 → (∀𝑥(𝜑𝜓) → [𝐴 / 𝑥](𝜑𝜓)))
41, 2, 3e12 44744 . . . 4 (   𝐴𝐵   ,   𝑥(𝜑𝜓)   ▶   [𝐴 / 𝑥](𝜑𝜓)   )
5 sbcbig 3840 . . . . 5 (𝐴𝐵 → ([𝐴 / 𝑥](𝜑𝜓) ↔ ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓)))
65biimpd 229 . . . 4 (𝐴𝐵 → ([𝐴 / 𝑥](𝜑𝜓) → ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓)))
71, 4, 6e12 44744 . . 3 (   𝐴𝐵   ,   𝑥(𝜑𝜓)   ▶   ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓)   )
87in2 44625 . 2 (   𝐴𝐵   ▶   (∀𝑥(𝜑𝜓) → ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓))   )
98in1 44591 1 (𝐴𝐵 → (∀𝑥(𝜑𝜓) → ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wal 1538  wcel 2108  [wsbc 3788
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-12 2177  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-sbc 3789  df-vd1 44590  df-vd2 44598
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator