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

Theorem sbbii 1804
Description: Infer substitution into both sides of a logical equivalence. (Contributed by NM, 14-May-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 198 . . 3  |-  ( ph  ->  ps )
32sbimi 1803 . 2  |-  ( [ y  /  x ] ph  ->  [ y  /  x ] ps )
41biimpri 210 . . 3  |-  ( ps 
->  ph )
54sbimi 1803 . 2  |-  ( [ y  /  x ] ps  ->  [ y  /  x ] ph )
63, 5impbii 191 1  |-  ( [ y  /  x ] ph 
<->  [ y  /  x ] ps )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 188   [wsb 1797
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682
This theorem depends on definitions:  df-bi 189  df-an 373  df-ex 1664  df-sb 1798
This theorem is referenced by:  sbor  2227  sban  2228  sb3an  2229  sbbi  2230  sbco  2241  sbidm  2243  sbco2d  2245  sbco3  2246  equsb3  2261  equsb3ALT  2262  elsb3  2263  elsb4  2264  sbcom4  2275  sb7f  2282  sbex  2292  sbco4lem  2294  sbco4  2295  sbmo  2344  eqsb3  2556  clelsb3  2557  cbvab  2574  sbabel  2620  sbabelOLD  2621  sbralie  3032  sbcco  3290  exss  4663  inopab  4965  isarep1  5662  clelsb3f  28116  bj-sbnf  31441  bj-clelsb3  31457  bj-sbeq  31503  bj-snsetex  31557  2uasbanh  36928  2uasbanhVD  37308
  Copyright terms: Public domain W3C validator