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

Theorem sbbii 1873
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 204 . . 3 (𝜑𝜓)
32sbimi 1872 . 2 ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓)
41biimpri 216 . . 3 (𝜓𝜑)
54sbimi 1872 . 2 ([𝑦 / 𝑥]𝜓 → [𝑦 / 𝑥]𝜑)
63, 5impbii 197 1 ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 194  [wsb 1866
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727
This theorem depends on definitions:  df-bi 195  df-an 384  df-ex 1695  df-sb 1867
This theorem is referenced by:  sbor  2385  sban  2386  sb3an  2387  sbbi  2388  sbco  2399  sbidm  2401  sbco2d  2403  sbco3  2404  equsb3  2419  equsb3ALT  2420  elsb3  2421  elsb4  2422  sbcom4  2433  sb7f  2440  sbex  2450  sbco4lem  2452  sbco4  2453  sbmo  2502  eqsb3  2714  clelsb3  2715  cbvab  2732  sbabel  2778  sbralie  3159  sbcco  3424  exss  4852  inopab  5162  isarep1  5877  clelsb3f  28510  bj-sbnf  31822  bj-clelsb3  31838  bj-sbeq  31884  bj-snsetex  31940  2uasbanh  37594  2uasbanhVD  37965
  Copyright terms: Public domain W3C validator