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

Theorem sbbii 2072
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 215 . . 3 (𝜑𝜓)
32sbimi 2070 . 2 ([𝑡 / 𝑥]𝜑 → [𝑡 / 𝑥]𝜓)
41biimpri 227 . . 3 (𝜓𝜑)
54sbimi 2070 . 2 ([𝑡 / 𝑥]𝜓 → [𝑡 / 𝑥]𝜑)
63, 5impbii 208 1 ([𝑡 / 𝑥]𝜑 ↔ [𝑡 / 𝑥]𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 205  [wsb 2060
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804
This theorem depends on definitions:  df-bi 206  df-sb 2061
This theorem is referenced by:  2sbbii  2073  sb3an  2077  sbcom4  2085  sbievw2  2092  sbco4lem  2164  sbco4  2165  sbcov  2244  sbco4lemOLD  2268  sbex  2271  sbor  2297  sbbi  2298  sbnf  2302  sbnfOLD  2303  cbvsbv  2354  sbco  2501  sbidm  2504  sbco2d  2506  sbco3  2507  sb7f  2519  sbmo  2603  cbvab  2801  clelsb2OLD  2855  clelsb1fw  2896  clelsb1f  2897  sbabel  2928  sbabelOLD  2929  sbralie  3342  sbralieALT  3343  sbccow  3799  sbcco  3802  exss  5469  inopab  5835  difopab  5836  isarep1OLD  6649  xpab  35548  bj-sbeq  36607  bj-snsetex  36670  2uasbanh  44237  2uasbanhVD  44587  2reu8i  46726  ichv  47021  ichf  47022  ichid  47023  ichcircshi  47026  ichan  47027  ichn  47028  ichbi12i  47032  icheq  47034  ichal  47038  ichnreuop  47044  ichreuopeq  47045
  Copyright terms: Public domain W3C validator