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

Theorem sbbii 1733
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 194 . . 3  |-  ( ph  ->  ps )
32sbimi 1732 . 2  |-  ( [ y  /  x ] ph  ->  [ y  /  x ] ps )
41biimpri 206 . . 3  |-  ( ps 
->  ph )
54sbimi 1732 . 2  |-  ( [ y  /  x ] ps  ->  [ y  /  x ] ph )
63, 5impbii 188 1  |-  ( [ y  /  x ] ph 
<->  [ y  /  x ] ps )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184   [wsb 1726
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1600  df-sb 1727
This theorem is referenced by:  sbor  2125  sban  2126  sb3an  2127  sbbi  2128  sbco  2140  sbidm  2142  sbco2d  2145  sbco3  2146  equsb3  2162  equsb3ALT  2163  elsb3  2164  elsb4  2165  sbcom4  2176  sb7f  2183  sbex  2193  sbco4lem  2195  sbco4  2196  sbmo  2321  2eu6OLD  2370  eqsb3  2563  clelsb3  2564  cbvab  2584  sbabel  2636  sbabelOLD  2637  sbralie  3083  sbcco  3336  exss  4700  inopab  5123  isarep1  5657  clelsb3f  27357  2uasbanh  33202  2uasbanhVD  33579  bj-sbnf  34295  bj-clelsb3  34307  bj-sbeq  34351  bj-snsetex  34404  frege72  37767
  Copyright terms: Public domain W3C validator