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

Theorem sbbii 2052
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 217 . . 3 (𝜑𝜓)
32sbimi 2050 . 2 ([𝑡 / 𝑥]𝜑 → [𝑡 / 𝑥]𝜓)
41biimpri 229 . . 3 (𝜓𝜑)
54sbimi 2050 . 2 ([𝑡 / 𝑥]𝜓 → [𝑡 / 𝑥]𝜑)
63, 5impbii 210 1 ([𝑡 / 𝑥]𝜑 ↔ [𝑡 / 𝑥]𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 207  [wsb 2040
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789
This theorem depends on definitions:  df-bi 208  df-sb 2041
This theorem is referenced by:  2sbbii  2053  sb3an  2058  sbcom4  2068  sbievw2  2072  equsb3rOLD  2076  sbcov  2219  sbco4lem  2247  sbco4  2248  sbex  2252  sbanOLD  2276  sbor  2279  sbbi  2280  sbanvOLD  2289  sbbivOLD  2290  sbco  2501  sbidm  2504  sbco2d  2506  sbco3  2507  sb7f  2519  sbmo  2664  clelsb3vOLD  2909  cbvabv  2925  cbvab  2926  clelsb3f  2951  clelsb3fOLD  2952  sbabel  2981  sbralie  3414  sbcco  3724  exss  5240  inopab  5579  isarep1  6304  bj-sbnf  33678  bj-sbeq  33733  bj-snsetex  33826  wl-clelsb3df  34340  2uasbanh  40386  2uasbanhVD  40736  2reu8i  42782  ichv  43045  ichf  43046  ichid  43047  ichcircshi  43048  ichbi12i  43054  icheq  43056  ichn  43062  ichal  43063  ichan  43066  ichnreuop  43070  ichreuopeq  43071
  Copyright terms: Public domain W3C validator