MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sbbii Structured version   Visualization version   GIF version

Theorem sbbii 2076
Description: Infer substitution into both sides of a logical equivalence. (Contributed by NM, 14-May-1993.)
Hypothesis
Ref Expression
sbbii.1 (𝜑𝜓)
Assertion
Ref Expression
sbbii ([𝑡 / 𝑥]𝜑 ↔ [𝑡 / 𝑥]𝜓)

Proof of Theorem sbbii
StepHypRef Expression
1 sbbii.1 . . . 4 (𝜑𝜓)
21biimpi 216 . . 3 (𝜑𝜓)
32sbimi 2074 . 2 ([𝑡 / 𝑥]𝜑 → [𝑡 / 𝑥]𝜓)
41biimpri 228 . . 3 (𝜓𝜑)
54sbimi 2074 . 2 ([𝑡 / 𝑥]𝜓 → [𝑡 / 𝑥]𝜑)
63, 5impbii 209 1 ([𝑡 / 𝑥]𝜑 ↔ [𝑡 / 𝑥]𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 206  [wsb 2064
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809
This theorem depends on definitions:  df-bi 207  df-sb 2065
This theorem is referenced by:  2sbbii  2077  sb3an  2081  sbcom4  2089  sbievw2  2098  cbvsbv  2100  sbco4lemOLD  2174  sbco4OLD  2175  sbcovOLD  2257  sbex  2281  sbor  2307  sbbi  2308  sbnf  2312  sbnfOLD  2313  sbco  2512  sbidm  2515  sbco2d  2517  sbco3  2518  sb7f  2530  sbmo  2614  cbvab  2814  clelsb2OLD  2870  clelsb1fw  2909  clelsb1f  2910  sbabel  2938  sbabelOLD  2939  sbralie  3358  sbralieALT  3359  sbccow  3811  sbcco  3814  exss  5468  inopab  5839  difopab  5840  isarep1OLD  6657  xpab  35726  bj-sbeq  36902  bj-snsetex  36964  2uasbanh  44581  2uasbanhVD  44931  2reu8i  47125  ichv  47436  ichf  47437  ichid  47438  ichcircshi  47441  ichan  47442  ichn  47443  ichbi12i  47447  icheq  47449  ichal  47453  ichnreuop  47459  ichreuopeq  47460
  Copyright terms: Public domain W3C validator