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

Theorem sbbii 1648
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 113 . . 3 (𝜑𝜓)
32sbimi 1647 . 2 ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓)
41biimpri 124 . . 3 (𝜓𝜑)
54sbimi 1647 . 2 ([𝑦 / 𝑥]𝜓 → [𝑦 / 𝑥]𝜑)
63, 5impbii 117 1 ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜓)
Colors of variables: wff set class
Syntax hints:  wb 98  [wsb 1645
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 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-ial 1427
This theorem depends on definitions:  df-bi 110  df-sb 1646
This theorem is referenced by:  sbco2v  1821  equsb3  1825  sbn  1826  sbim  1827  sbor  1828  sban  1829  sb3an  1832  sbbi  1833  sbco2h  1838  sbco2d  1840  sbco2vd  1841  sbco3v  1843  sbco3  1848  elsb3  1852  elsb4  1853  sbcom2v2  1862  sbcom2  1863  dfsb7  1867  sb7f  1868  sb7af  1869  sbal  1876  sbal1  1878  sbex  1880  sbco4lem  1882  sbco4  1883  sbmo  1959  eqsb3  2141  clelsb3  2142  clelsb4  2143  sbabel  2203  sbralie  2546  sbcco  2785  exss  3963  inopab  4468  isarep1  4985
  Copyright terms: Public domain W3C validator