Theorem sbbii 1887

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

Syntax hints:   ↔ wb 196  [wsb 1880

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

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-sb 1881

This theorem is referenced by:  sbor  2398  sban  2399  sb3an  2400  sbbi  2401  sbco  2412  sbidm  2414  sbco2d  2416  sbco3  2417  equsb3  2432  equsb3ALT  2433  elsb3  2434  elsb4  2435  sbcom4  2446  sb7f  2453  sbex  2463  sbco4lem  2465  sbco4  2466  sbmo  2515  eqsb3  2728  clelsb3  2729  cbvab  2746  clelsb3f  2768  sbabel  2793  sbralie  3184  sbcco  3458  exss  4931  inopab  5252  isarep1  5977  bj-sbnf  32828  bj-clelsb3  32848  bj-sbeq  32896  bj-snsetex  32951  2uasbanh  38777  2uasbanhVD  39147