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

Theorem sbbii 1884
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 1883 . 2 ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓)
41biimpri 218 . . 3 (𝜓𝜑)
54sbimi 1883 . 2 ([𝑦 / 𝑥]𝜓 → [𝑦 / 𝑥]𝜑)
63, 5impbii 199 1 ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 196  [wsb 1877
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1702  df-sb 1878
This theorem is referenced by:  sbor  2397  sban  2398  sb3an  2399  sbbi  2400  sbco  2411  sbidm  2413  sbco2d  2415  sbco3  2416  equsb3  2431  equsb3ALT  2432  elsb3  2433  elsb4  2434  sbcom4  2445  sb7f  2452  sbex  2462  sbco4lem  2464  sbco4  2465  sbmo  2514  eqsb3  2725  clelsb3  2726  cbvab  2743  sbabel  2789  sbralie  3176  sbcco  3445  exss  4902  inopab  5222  isarep1  5945  clelsb3f  29209  bj-sbnf  32524  bj-clelsb3  32548  bj-sbeq  32596  bj-snsetex  32651  2uasbanh  38298  2uasbanhVD  38669
  Copyright terms: Public domain W3C validator