Theorem sbbii 1763

Description: Infer substitution into both sides of a logical equivalence. (Contributed by NM, 5-Aug-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 120	. . 3 ⊢ (𝜑 → 𝜓)
3	2	sbimi 1762	. 2 ⊢ ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓)
4	1	biimpri 133	. . 3 ⊢ (𝜓 → 𝜑)
5	4	sbimi 1762	. 2 ⊢ ([𝑦 / 𝑥]𝜓 → [𝑦 / 𝑥]𝜑)
6	3, 5	impbii 126	1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜓)

Syntax hints:   ↔ wb 105  [wsb 1760

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1445  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-4 1508  ax-ial 1532

This theorem depends on definitions:  df-bi 117  df-sb 1761

This theorem is referenced by:  sbco2vh  1943  equsb3  1949  sbn  1950  sbim  1951  sbor  1952  sban  1953  sb3an  1956  sbbi  1957  sbco2h  1962  sbco2d  1964  sbco2vd  1965  sbco3v  1967  sbco3  1972  sbcom2v2  1984  sbcom2  1985  dfsb7  1989  sb7f  1990  sb7af  1991  sbal  1998  sbal1  2000  sbex  2002  sbco4lem  2004  sbco4  2005  sbmo  2083  elsb1  2153  elsb2  2154  eqsb1  2279  clelsb1  2280  clelsb2  2281  cbvabw  2298  clelsb1f  2321  sbabel  2344  sbralie  2719  sbcco  2982  exss  4221  inopab  4752  isarep1  5294  bezoutlemnewy  11962