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

Theorem sbbii 1738
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 ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜓)

Proof of Theorem sbbii
StepHypRef Expression
1 sbbii.1 . . . 4 (𝜑𝜓)
21biimpi 119 . . 3 (𝜑𝜓)
32sbimi 1737 . 2 ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓)
41biimpri 132 . . 3 (𝜓𝜑)
54sbimi 1737 . 2 ([𝑦 / 𝑥]𝜓 → [𝑦 / 𝑥]𝜑)
63, 5impbii 125 1 ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜓)
Colors of variables: wff set class
Syntax hints:  wb 104  [wsb 1735
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 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-ial 1514
This theorem depends on definitions:  df-bi 116  df-sb 1736
This theorem is referenced by:  sbco2vh  1918  equsb3  1924  sbn  1925  sbim  1926  sbor  1927  sban  1928  sb3an  1931  sbbi  1932  sbco2h  1937  sbco2d  1939  sbco2vd  1940  sbco3v  1942  sbco3  1947  elsb3  1951  elsb4  1952  sbcom2v2  1961  sbcom2  1962  dfsb7  1966  sb7f  1967  sb7af  1968  sbal  1975  sbal1  1977  sbex  1979  sbco4lem  1981  sbco4  1982  sbmo  2058  eqsb3  2243  clelsb3  2244  clelsb4  2245  cbvabw  2262  clelsb3f  2285  sbabel  2307  sbralie  2670  sbcco  2930  exss  4149  inopab  4671  isarep1  5209  bezoutlemnewy  11691
  Copyright terms: Public domain W3C validator