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

Theorem sbbii 2056
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 206 . . 3 (𝜑𝜓)
32sbimi 2055 . 2 ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓)
41biimpri 218 . . 3 (𝜓𝜑)
54sbimi 2055 . 2 ([𝑦 / 𝑥]𝜓 → [𝑦 / 𝑥]𝜑)
63, 5impbii 199 1 ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 196  [wsb 2049
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885
This theorem depends on definitions:  df-bi 197  df-an 383  df-ex 1853  df-sb 2050
This theorem is referenced by:  sbor  2545  sban  2546  sb3an  2547  sbbi  2548  sbco  2559  sbidm  2561  sbco2d  2563  sbco3  2564  equsb3  2580  equsb3ALT  2581  elsb3  2583  elsb3OLD  2584  elsb4  2586  elsb4OLD  2587  sbcom4  2594  sb7f  2601  sbex  2611  sbco4lem  2613  sbco4  2614  sbmo  2664  eqsb3  2877  clelsb3  2878  cbvab  2895  clelsb3f  2917  sbabel  2942  sbralie  3333  sbcco  3610  exss  5059  inopab  5391  isarep1  6117  bj-sbnf  33163  bj-sbeq  33225  bj-snsetex  33282  2uasbanh  39302  2uasbanhVD  39669
  Copyright terms: Public domain W3C validator