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

Theorem sbbii 1718
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 1717 . 2  |-  ( [ y  /  x ] ph  ->  [ y  /  x ] ps )
41biimpri 206 . . 3  |-  ( ps 
->  ph )
54sbimi 1717 . 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 1711
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-sb 1712
This theorem is referenced by:  sbnOLD  2106  sbor  2113  sban  2114  sb3an  2115  sbbi  2116  sbco  2129  sbidm  2132  sbco2d  2136  sbco3  2137  sbco3OLD  2138  equsb3  2159  equsb3ALT  2160  elsb3  2161  elsb4  2162  sbcom4  2175  sb7f  2185  sbex  2198  sbco4lem  2200  sbco4  2201  sbmo  2337  2eu6OLD  2394  eqsb3  2587  clelsb3  2588  cbvab  2608  sbabel  2660  sbabelOLD  2661  sbralie  3106  sbcco  3359  exss  4716  inopab  5139  isarep1  5673  clelsb3f  27193  2uasbanh  32770  2uasbanhVD  33147  bj-sbnf  33849  bj-clelsb3  33861  bj-sbeq  33905  bj-snsetex  33958
  Copyright terms: Public domain W3C validator