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

Theorem sbbii 1709
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 1708 . 2  |-  ( [ y  /  x ] ph  ->  [ y  /  x ] ps )
41biimpri 206 . . 3  |-  ( ps 
->  ph )
54sbimi 1708 . 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 1702
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1588  df-sb 1703
This theorem is referenced by:  sbnOLD  2093  sbor  2100  sban  2101  sb3an  2102  sbbi  2103  sbco  2116  sbidm  2119  sbco2d  2123  sbco3  2124  sbco3OLD  2125  equsb3  2146  equsb3ALT  2147  elsb3  2148  elsb4  2149  sbcom4  2162  sb7f  2172  sbex  2185  sbco4lem  2187  sbco4  2188  sbmo  2324  2eu6OLD  2381  eqsb3  2574  clelsb3  2575  cbvab  2595  sbabel  2647  sbralie  3066  sbcco  3317  exss  4666  inopab  5081  isarep1  5608  clelsb3f  26036  2uasbanh  31622  2uasbanhVD  31999  bj-sbnf  32699  bj-clelsb3  32711  bj-sbeq  32755  bj-snsetex  32808
  Copyright terms: Public domain W3C validator