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

Theorem sbbii 1643
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 186 . . 3  |-  ( ph  ->  ps )
32sbimi 1642 . 2  |-  ( [ y  /  x ] ph  ->  [ y  /  x ] ps )
41biimpri 197 . . 3  |-  ( ps 
->  ph )
54sbimi 1642 . 2  |-  ( [ y  /  x ] ps  ->  [ y  /  x ] ph )
63, 5impbii 180 1  |-  ( [ y  /  x ] ph 
<->  [ y  /  x ] ps )
Colors of variables: wff set class
Syntax hints:    <-> wb 176   [wsb 1638
This theorem is referenced by:  sbn  2015  sbor  2019  sban  2022  sb3an  2023  sbbi  2024  sbco2d  2040  sbco3  2041  equsb3  2054  elsb3  2055  elsb4  2056  dfsb7  2071  sb7f  2072  sbex  2080  sbmo  2186  2eu6  2241  eqsb3  2397  clelsb3  2398  sbabel  2458  sbralie  2790  sbcco  3026  exss  4252  inopab  4832  isarep1  5347  clelsb3f  23158  2uasbanh  28626  2uasbanhVD  29003  sbnNEW7  29537  sborNEW7  29541  sbanNEW7  29544  sbbiNEW7  29545  sbco2dwAUX7  29560  sbco3wAUX7  29561  equsb3NEW7  29574  elsb3NEW7  29575  elsb4NEW7  29576  sbexNEW7  29589  sb3anNEW7  29611  sbco2dOLD7  29707  sbco3OLD7  29708  dfsb7OLD7  29719  sb7fOLD7  29720
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1532  df-sb 1639
  Copyright terms: Public domain W3C validator