MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sbbii Unicode version

Theorem sbbii 1660
Description: Infer substitution into both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
sbbii.1  |-  ( ph  <->  ps )
Assertion
Ref Expression
sbbii  |-  ( [ y  /  x ] ph 
<->  [ y  /  x ] ps )

Proof of Theorem sbbii
StepHypRef Expression
1 sbbii.1 . . . 4  |-  ( ph  <->  ps )
21biimpi 187 . . 3  |-  ( ph  ->  ps )
32sbimi 1659 . 2  |-  ( [ y  /  x ] ph  ->  [ y  /  x ] ps )
41biimpri 198 . . 3  |-  ( ps 
->  ph )
54sbimi 1659 . 2  |-  ( [ y  /  x ] ps  ->  [ y  /  x ] ph )
63, 5impbii 181 1  |-  ( [ y  /  x ] ph 
<->  [ y  /  x ] ps )
Colors of variables: wff set class
Syntax hints:    <-> wb 177   [wsb 1655
This theorem is referenced by:  sbn  2088  sbor  2092  sban  2095  sb3an  2096  sbbi  2097  sbco2d  2113  sbco3  2114  equsb3  2128  elsb3  2129  elsb4  2130  pm11.07  2141  dfsb7  2146  sb7f  2147  sbex  2155  sbmo  2261  2eu6  2316  eqsb3  2481  clelsb3  2482  sbabel  2542  sbralie  2881  sbcco  3119  exss  4360  inopab  4938  isarep1  5465  clelsb3f  23808  2uasbanh  27984  2uasbanhVD  28357  sbnNEW7  28891  sborNEW7  28895  sbanNEW7  28898  sbbiNEW7  28899  sbco2dwAUX7  28914  sbco3wAUX7  28915  equsb3NEW7  28928  elsb3NEW7  28929  elsb4NEW7  28930  sbexNEW7  28943  sb3anNEW7  28966  sbco2dOLD7  29062  sbco3OLD7  29063  dfsb7OLD7  29073  sb7fOLD7  29074
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-sb 1656
  Copyright terms: Public domain W3C validator