Theorem sbbii 1874

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

Step	Hyp	Ref	Expression
1		sbbii.1	. . . 4 ⊢ (𝜑 ↔ 𝜓)
2	1	biimpi 205	. . 3 ⊢ (𝜑 → 𝜓)
3	2	sbimi 1873	. 2 ⊢ ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓)
4	1	biimpri 217	. . 3 ⊢ (𝜓 → 𝜑)
5	4	sbimi 1873	. 2 ⊢ ([𝑦 / 𝑥]𝜓 → [𝑦 / 𝑥]𝜑)
6	3, 5	impbii 198	1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜓)

Syntax hints:   ↔ wb 195  [wsb 1867

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728

This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-sb 1868

This theorem is referenced by:  sbor  2386  sban  2387  sb3an  2388  sbbi  2389  sbco  2400  sbidm  2402  sbco2d  2404  sbco3  2405  equsb3  2420  equsb3ALT  2421  elsb3  2422  elsb4  2423  sbcom4  2434  sb7f  2441  sbex  2451  sbco4lem  2453  sbco4  2454  sbmo  2503  eqsb3  2715  clelsb3  2716  cbvab  2733  sbabel  2779  sbralie  3160  sbcco  3425  exss  4858  inopab  5174  isarep1  5891  clelsb3f  28704  bj-sbnf  32016  bj-clelsb3  32042  bj-sbeq  32088  bj-snsetex  32144  2uasbanh  37798  2uasbanhVD  38169