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

Theorem sbbii 1626
Description: Infer substitution into both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
sbbii.1 (φψ)
Assertion
Ref Expression
sbbii ([y / x]φ ↔ [y / x]ψ)

Proof of Theorem sbbii
StepHypRef Expression
1 sbbii.1 . . . 4 (φψ)
21biimpi 113 . . 3 (φψ)
32sbimi 1625 . 2 ([y / x]φ → [y / x]ψ)
41biimpri 124 . . 3 (ψφ)
54sbimi 1625 . 2 ([y / x]ψ → [y / x]φ)
63, 5impbii 117 1 ([y / x]φ ↔ [y / x]ψ)
Colors of variables: wff set class
Syntax hints:  wb 98  [wsb 1623
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1312  ax-gen 1314  ax-ie1 1359  ax-ie2 1360  ax-4 1377  ax-ial 1405
This theorem depends on definitions:  df-bi 110  df-sb 1624
This theorem is referenced by:  sbco2v  1799  equsb3  1803  sbn  1804  sbim  1805  sbor  1806  sban  1807  sb3an  1810  sbbi  1811  sbco2h  1816  sbco2d  1818  sbco2vd  1819  sbco3v  1821  sbco3  1826  elsb3  1830  elsb4  1831  sbcom2v2  1840  sbcom2  1841  dfsb7  1845  sb7f  1846  sb7af  1847  sbal  1854  sbal1  1856  sbex  1858  sbco4lem  1860  sbco4  1861  sbmo  1937  eqsb3  2119  clelsb3  2120  clelsb4  2121  sbabel  2181  sbralie  2520  sbcco  2758  exss  3933  inopab  4391  isarep1  4907
  Copyright terms: Public domain W3C validator