ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  sbbii Unicode version

Theorem sbbii 1721
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 119 . . 3  |-  ( ph  ->  ps )
32sbimi 1720 . 2  |-  ( [ y  /  x ] ph  ->  [ y  /  x ] ps )
41biimpri 132 . . 3  |-  ( ps 
->  ph )
54sbimi 1720 . 2  |-  ( [ y  /  x ] ps  ->  [ y  /  x ] ph )
63, 5impbii 125 1  |-  ( [ y  /  x ] ph 
<->  [ y  /  x ] ps )
Colors of variables: wff set class
Syntax hints:    <-> wb 104   [wsb 1718
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1406  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-4 1470  ax-ial 1497
This theorem depends on definitions:  df-bi 116  df-sb 1719
This theorem is referenced by:  sbco2v  1896  equsb3  1900  sbn  1901  sbim  1902  sbor  1903  sban  1904  sb3an  1907  sbbi  1908  sbco2h  1913  sbco2d  1915  sbco2vd  1916  sbco3v  1918  sbco3  1923  elsb3  1927  elsb4  1928  sbcom2v2  1937  sbcom2  1938  dfsb7  1942  sb7f  1943  sb7af  1944  sbal  1951  sbal1  1953  sbex  1955  sbco4lem  1957  sbco4  1958  sbmo  2034  eqsb3  2219  clelsb3  2220  clelsb4  2221  clelsb3f  2260  sbabel  2282  sbralie  2642  sbcco  2901  exss  4117  inopab  4639  isarep1  5177  bezoutlemnewy  11580
  Copyright terms: Public domain W3C validator