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

Theorem sbbii 1723
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 1722 . 2 ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓)
41biimpri 132 . . 3 (𝜓𝜑)
54sbimi 1722 . 2 ([𝑦 / 𝑥]𝜓 → [𝑦 / 𝑥]𝜑)
63, 5impbii 125 1 ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜓)
Colors of variables: wff set class
Syntax hints:  wb 104  [wsb 1720
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 1408  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-4 1472  ax-ial 1499
This theorem depends on definitions:  df-bi 116  df-sb 1721
This theorem is referenced by:  sbco2v  1898  equsb3  1902  sbn  1903  sbim  1904  sbor  1905  sban  1906  sb3an  1909  sbbi  1910  sbco2h  1915  sbco2d  1917  sbco2vd  1918  sbco3v  1920  sbco3  1925  elsb3  1929  elsb4  1930  sbcom2v2  1939  sbcom2  1940  dfsb7  1944  sb7f  1945  sb7af  1946  sbal  1953  sbal1  1955  sbex  1957  sbco4lem  1959  sbco4  1960  sbmo  2036  eqsb3  2221  clelsb3  2222  clelsb4  2223  clelsb3f  2262  sbabel  2284  sbralie  2644  sbcco  2903  exss  4119  inopab  4641  isarep1  5179  bezoutlemnewy  11611
  Copyright terms: Public domain W3C validator