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

Theorem sbbii 2067
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 207 . . 3 (𝜑𝜓)
32sbimi 2066 . 2 ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓)
41biimpri 219 . . 3 (𝜓𝜑)
54sbimi 2066 . 2 ([𝑦 / 𝑥]𝜓 → [𝑦 / 𝑥]𝜑)
63, 5impbii 200 1 ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 197  [wsb 2060
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894
This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1860  df-sb 2061
This theorem is referenced by:  sbor  2557  sban  2558  sb3an  2559  sbbi  2560  sbco  2571  sbidm  2573  sbco2d  2575  sbco3  2576  equsb3  2592  equsb3ALT  2593  elsb3  2595  elsb3OLD  2596  elsb4  2598  elsb4OLD  2599  sbcom4  2606  sb7f  2613  sbex  2623  sbco4lem  2625  sbco4  2626  sbmo  2678  eqsb3  2912  clelsb3  2913  cbvab  2930  clelsb3f  2952  sbabel  2977  sbralie  3373  sbcco  3656  exss  5121  inopab  5454  isarep1  6188  bj-sbnf  33141  bj-sbeq  33204  bj-snsetex  33261  2uasbanh  39275  2uasbanhVD  39641
  Copyright terms: Public domain W3C validator