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

Theorem sbcbi 27968
Description: Implication form of sbcbiiOLD 3161. sbcbi 27968 is sbcbiVD 28330 without virtual deductions and was automatically derived from sbcbiVD 28330 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 3117 . 2  |-  ( A  e.  V  ->  ( A. x ( ph  <->  ps )  ->  [. A  /  x ]. ( ph  <->  ps )
) )
2 sbcbig 3151 . 2  |-  ( A  e.  V  ->  ( [. A  /  x ]. ( ph  <->  ps )  <->  (
[. A  /  x ]. ph  <->  [. A  /  x ]. ps ) ) )
31, 2sylibd 206 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 177   A.wal 1546    e. wcel 1717   [.wsbc 3105
This theorem is referenced by:  onfrALTlem5  27972  trsbcVD  28331  sbcssVD  28337  onfrALTlem5VD  28339
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2369
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2375  df-cleq 2381  df-clel 2384  df-nfc 2513  df-v 2902  df-sbc 3106
  Copyright terms: Public domain W3C validator