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

Theorem sbbii 1944
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 1943 . 2 ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓)
41biimpri 218 . . 3 (𝜓𝜑)
54sbimi 1943 . 2 ([𝑦 / 𝑥]𝜓 → [𝑦 / 𝑥]𝜑)
63, 5impbii 199 1 ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 196  [wsb 1937
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-sb 1938
This theorem is referenced by:  sbor  2426  sban  2427  sb3an  2428  sbbi  2429  sbco  2440  sbidm  2442  sbco2d  2444  sbco3  2445  equsb3  2460  equsb3ALT  2461  elsb3  2462  elsb4  2463  sbcom4  2474  sb7f  2481  sbex  2491  sbco4lem  2493  sbco4  2494  sbmo  2544  eqsb3  2757  clelsb3  2758  cbvab  2775  clelsb3f  2797  sbabel  2822  sbralie  3214  sbcco  3491  exss  4961  inopab  5285  isarep1  6015  bj-sbnf  32953  bj-clelsb3  32973  bj-sbeq  33021  bj-snsetex  33076  2uasbanh  39094  2uasbanhVD  39461
  Copyright terms: Public domain W3C validator