Theorem sbbii 2056

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 206	. . 3 ⊢ (𝜑 → 𝜓)
3	2	sbimi 2055	. 2 ⊢ ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓)
4	1	biimpri 218	. . 3 ⊢ (𝜓 → 𝜑)
5	4	sbimi 2055	. 2 ⊢ ([𝑦 / 𝑥]𝜓 → [𝑦 / 𝑥]𝜑)
6	3, 5	impbii 199	1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜓)

Syntax hints:   ↔ wb 196  [wsb 2049

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

This theorem depends on definitions:  df-bi 197  df-an 383  df-ex 1853  df-sb 2050

This theorem is referenced by:  sbor  2545  sban  2546  sb3an  2547  sbbi  2548  sbco  2559  sbidm  2561  sbco2d  2563  sbco3  2564  equsb3  2580  equsb3ALT  2581  elsb3  2583  elsb3OLD  2584  elsb4  2586  elsb4OLD  2587  sbcom4  2594  sb7f  2601  sbex  2611  sbco4lem  2613  sbco4  2614  sbmo  2664  eqsb3  2877  clelsb3  2878  cbvab  2895  clelsb3f  2917  sbabel  2942  sbralie  3333  sbcco  3610  exss  5059  inopab  5391  isarep1  6117  bj-sbnf  33163  bj-sbeq  33225  bj-snsetex  33282  2uasbanh  39302  2uasbanhVD  39669