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

Theorem sbbii 1874
 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 205 . . 3 (𝜑𝜓)
32sbimi 1873 . 2 ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓)
41biimpri 217 . . 3 (𝜓𝜑)
54sbimi 1873 . 2 ([𝑦 / 𝑥]𝜓 → [𝑦 / 𝑥]𝜑)
63, 5impbii 198 1 ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜓)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 195  [wsb 1867 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728 This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-sb 1868 This theorem is referenced by:  sbor  2386  sban  2387  sb3an  2388  sbbi  2389  sbco  2400  sbidm  2402  sbco2d  2404  sbco3  2405  equsb3  2420  equsb3ALT  2421  elsb3  2422  elsb4  2423  sbcom4  2434  sb7f  2441  sbex  2451  sbco4lem  2453  sbco4  2454  sbmo  2503  eqsb3  2715  clelsb3  2716  cbvab  2733  sbabel  2779  sbralie  3160  sbcco  3425  exss  4858  inopab  5174  isarep1  5891  clelsb3f  28704  bj-sbnf  32016  bj-clelsb3  32042  bj-sbeq  32088  bj-snsetex  32144  2uasbanh  37798  2uasbanhVD  38169
 Copyright terms: Public domain W3C validator