Theorem sbbii 2067

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

Syntax hints:   ↔ wb 197  [wsb 2060

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

This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1860  df-sb 2061

This theorem is referenced by:  sbor  2557  sban  2558  sb3an  2559  sbbi  2560  sbco  2571  sbidm  2573  sbco2d  2575  sbco3  2576  equsb3  2592  equsb3ALT  2593  elsb3  2595  elsb3OLD  2596  elsb4  2598  elsb4OLD  2599  sbcom4  2606  sb7f  2613  sbex  2623  sbco4lem  2625  sbco4  2626  sbmo  2678  eqsb3  2912  clelsb3  2913  cbvab  2930  clelsb3f  2952  sbabel  2977  sbralie  3373  sbcco  3656  exss  5121  inopab  5454  isarep1  6188  bj-sbnf  33141  bj-sbeq  33204  bj-snsetex  33261  2uasbanh  39275  2uasbanhVD  39641