Theorem sbbii 1776

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

Syntax hints:   ↔ wb 105  [wsb 1773

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-ial 1545

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

This theorem is referenced by:  sbco2vh  1957  equsb3  1963  sbn  1964  sbim  1965  sbor  1966  sban  1967  sb3an  1970  sbbi  1971  sbco2h  1976  sbco2d  1978  sbco2vd  1979  sbco3v  1981  sbco3  1986  sbcom2v2  1998  sbcom2  1999  dfsb7  2003  sb7f  2004  sb7af  2005  sbal  2012  sbal1  2014  sbex  2016  sbco4lem  2018  sbco4  2019  sbmo  2097  elsb1  2167  elsb2  2168  eqsb1  2293  clelsb1  2294  clelsb2  2295  cbvabw  2312  clelsb1f  2336  sbabel  2359  sbralie  2740  sbcco  3003  exss  4252  inopab  4784  isarep1  5328  bezoutlemnewy  12044