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

Theorem sbbii 2081
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 219 . . 3 (𝜑𝜓)
32sbimi 2079 . 2 ([𝑡 / 𝑥]𝜑 → [𝑡 / 𝑥]𝜓)
41biimpri 231 . . 3 (𝜓𝜑)
54sbimi 2079 . 2 ([𝑡 / 𝑥]𝜓 → [𝑡 / 𝑥]𝜑)
63, 5impbii 212 1 ([𝑡 / 𝑥]𝜑 ↔ [𝑡 / 𝑥]𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 209  [wsb 2069
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811
This theorem depends on definitions:  df-bi 210  df-sb 2070
This theorem is referenced by:  2sbbii  2082  sb3an  2086  sbcom4  2097  sbievw2  2105  equsb3rOLD  2109  sbcov  2257  sbco4lem  2281  sbco4  2282  sbex  2286  sbanOLD  2310  sbor  2314  sbbi  2315  sbanvOLD  2321  sbbivOLD  2322  sbco  2529  sbidm  2532  sbco2d  2534  sbco3  2535  sb7f  2548  sbmo  2678  cbvabv  2869  cbvabwOLD  2871  cbvab  2872  clelsb3vOLD  2921  clelsb3fw  2962  clelsb3f  2963  sbabel  2989  sbralie  3421  sbccow  3746  sbcco  3749  exss  5323  inopab  5669  isarep1  6416  bj-sbnf  34274  bj-sbeq  34337  bj-snsetex  34394  wl-clelsb3df  35021  2uasbanh  41254  2uasbanhVD  41604  2reu8i  43656  ichv  43953  ichf  43954  ichid  43955  ichcircshi  43958  ichan  43959  ichn  43960  ichbi12i  43964  icheq  43966  ichal  43970  ichnreuop  43976  ichreuopeq  43977
  Copyright terms: Public domain W3C validator