Theorem sbbii 1944

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

Syntax hints:   ↔ wb 196  [wsb 1937

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

This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-sb 1938

This theorem is referenced by:  sbor  2426  sban  2427  sb3an  2428  sbbi  2429  sbco  2440  sbidm  2442  sbco2d  2444  sbco3  2445  equsb3  2460  equsb3ALT  2461  elsb3  2462  elsb4  2463  sbcom4  2474  sb7f  2481  sbex  2491  sbco4lem  2493  sbco4  2494  sbmo  2544  eqsb3  2757  clelsb3  2758  cbvab  2775  clelsb3f  2797  sbabel  2822  sbralie  3214  sbcco  3491  exss  4961  inopab  5285  isarep1  6015  bj-sbnf  32953  bj-clelsb3  32973  bj-sbeq  33021  bj-snsetex  33076  2uasbanh  39094  2uasbanhVD  39461