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

Theorem sbbii 1665
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 1664 . 2  |-  ( [ y  /  x ] ph  ->  [ y  /  x ] ps )
41biimpri 198 . . 3  |-  ( ps 
->  ph )
54sbimi 1664 . 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 1658
This theorem is referenced by:  sbnOLD  2118  sbor  2140  sban  2143  sb3an  2144  sbbi  2145  sbco2d  2162  sbco3  2163  equsb3  2177  elsb3  2178  elsb4  2179  pm11.07  2190  sb7f  2195  sbex  2204  sbmo  2310  2eu6  2365  eqsb3  2536  clelsb3  2537  sbabel  2597  sbralie  2937  sbcco  3175  exss  4418  inopab  4997  isarep1  5524  clelsb3f  23963  2uasbanh  28585  2uasbanhVD  28960  sbnNEW7  29499  sborNEW7  29503  sbanNEW7  29506  sbbiNEW7  29507  sbco2dwAUX7  29523  sbco3wAUX7  29524  equsb3NEW7  29539  elsb3NEW7  29540  elsb4NEW7  29541  sbexNEW7  29554  sb3anNEW7  29577  ax7w14lemAUX7  29606  elsb34AUX7  29609  ax7w17lem1AUX7  29612  sbco2dOLD7  29690  sbco3OLD7  29691  dfsb7OLD7  29700  sb7fOLD7  29701
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-sb 1659
  Copyright terms: Public domain W3C validator