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

Theorem sbbii 1765
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 120 . . 3 (𝜑𝜓)
32sbimi 1764 . 2 ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓)
41biimpri 133 . . 3 (𝜓𝜑)
54sbimi 1764 . 2 ([𝑦 / 𝑥]𝜓 → [𝑦 / 𝑥]𝜑)
63, 5impbii 126 1 ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜓)
Colors of variables: wff set class
Syntax hints:  wb 105  [wsb 1762
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-ial 1534
This theorem depends on definitions:  df-bi 117  df-sb 1763
This theorem is referenced by:  sbco2vh  1945  equsb3  1951  sbn  1952  sbim  1953  sbor  1954  sban  1955  sb3an  1958  sbbi  1959  sbco2h  1964  sbco2d  1966  sbco2vd  1967  sbco3v  1969  sbco3  1974  sbcom2v2  1986  sbcom2  1987  dfsb7  1991  sb7f  1992  sb7af  1993  sbal  2000  sbal1  2002  sbex  2004  sbco4lem  2006  sbco4  2007  sbmo  2085  elsb1  2155  elsb2  2156  eqsb1  2281  clelsb1  2282  clelsb2  2283  cbvabw  2300  clelsb1f  2323  sbabel  2346  sbralie  2721  sbcco  2984  exss  4227  inopab  4759  isarep1  5302  bezoutlemnewy  11996
  Copyright terms: Public domain W3C validator