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

Theorem sbbii 1634
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 1633 . 2  |-  ( [ y  /  x ] ph  ->  [ y  /  x ] ps )
41biimpri 197 . . 3  |-  ( ps 
->  ph )
54sbimi 1633 . 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 1629
This theorem is referenced by:  sbn  2002  sbor  2006  sban  2009  sb3an  2010  sbbi  2011  sbco2d  2027  sbco3  2028  equsb3  2041  elsb3  2042  elsb4  2043  dfsb7  2058  sb7f  2059  sbex  2067  sbmo  2173  2eu6  2228  eqsb3  2384  clelsb3  2385  sbabel  2445  sbralie  2777  sbcco  3013  exss  4236  inopab  4816  isarep1  5331  clelsb3f  23142  2uasbanh  28327  2uasbanhVD  28687
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-sb 1630
  Copyright terms: Public domain W3C validator