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

Theorem sbbii 1695
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 118 . . 3  |-  ( ph  ->  ps )
32sbimi 1694 . 2  |-  ( [ y  /  x ] ph  ->  [ y  /  x ] ps )
41biimpri 131 . . 3  |-  ( ps 
->  ph )
54sbimi 1694 . 2  |-  ( [ y  /  x ] ps  ->  [ y  /  x ] ph )
63, 5impbii 124 1  |-  ( [ y  /  x ] ph 
<->  [ y  /  x ] ps )
Colors of variables: wff set class
Syntax hints:    <-> wb 103   [wsb 1692
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-4 1445  ax-ial 1472
This theorem depends on definitions:  df-bi 115  df-sb 1693
This theorem is referenced by:  sbco2v  1869  equsb3  1873  sbn  1874  sbim  1875  sbor  1876  sban  1877  sb3an  1880  sbbi  1881  sbco2h  1886  sbco2d  1888  sbco2vd  1889  sbco3v  1891  sbco3  1896  elsb3  1900  elsb4  1901  sbcom2v2  1910  sbcom2  1911  dfsb7  1915  sb7f  1916  sb7af  1917  sbal  1924  sbal1  1926  sbex  1928  sbco4lem  1930  sbco4  1931  sbmo  2007  eqsb3  2191  clelsb3  2192  clelsb4  2193  clelsb3f  2232  sbabel  2254  sbralie  2603  sbcco  2861  exss  4054  inopab  4568  isarep1  5100  bezoutlemnewy  11259
  Copyright terms: Public domain W3C validator