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

Theorem sbcbi 28602
Description: Implication form of sbcbiiOLD 3060. sbcbi 28602 is sbcbiVD 28968 without virtual deductions and was automatically derived from sbcbiVD 28968 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  |-  ( A  e.  V  ->  ( A. x ( ph  <->  ps )  ->  ( [. A  /  x ]. ph  <->  [. A  /  x ]. ps ) ) )

Proof of Theorem sbcbi
StepHypRef Expression
1 spsbc 3016 . 2  |-  ( A  e.  V  ->  ( A. x ( ph  <->  ps )  ->  [. A  /  x ]. ( ph  <->  ps )
) )
2 sbcbig 3050 . 2  |-  ( A  e.  V  ->  ( [. A  /  x ]. ( ph  <->  ps )  <->  (
[. A  /  x ]. ph  <->  [. A  /  x ]. ps ) ) )
31, 2sylibd 205 1  |-  ( A  e.  V  ->  ( A. x ( ph  <->  ps )  ->  ( [. A  /  x ]. ph  <->  [. A  /  x ]. ps ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176   A.wal 1530    e. wcel 1696   [.wsbc 3004
This theorem is referenced by:  onfrALTlem5  28606  trsbcVD  28969  sbcssVD  28975  onfrALTlem5VD  28977
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-sbc 3005
  Copyright terms: Public domain W3C validator