Theorem sbbii 1739

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

Syntax hints:   ↔ wb 104  [wsb 1736

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1488  ax-ial 1515

This theorem depends on definitions:  df-bi 116  df-sb 1737

This theorem is referenced by:  sbco2vh  1919  equsb3  1925  sbn  1926  sbim  1927  sbor  1928  sban  1929  sb3an  1932  sbbi  1933  sbco2h  1938  sbco2d  1940  sbco2vd  1941  sbco3v  1943  sbco3  1948  elsb3  1952  elsb4  1953  sbcom2v2  1962  sbcom2  1963  dfsb7  1967  sb7f  1968  sb7af  1969  sbal  1976  sbal1  1978  sbex  1980  sbco4lem  1982  sbco4  1983  sbmo  2059  eqsb3  2244  clelsb3  2245  clelsb4  2246  cbvabw  2263  clelsb3f  2286  sbabel  2308  sbralie  2673  sbcco  2934  exss  4157  inopab  4679  isarep1  5217  bezoutlemnewy  11720