Theorem sbbii 1811

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

Syntax hints:   ↔ wb 105  [wsb 1808

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-ial 1580

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

This theorem is referenced by:  sbco2vh  1996  equsb3  2002  sbn  2003  sbim  2004  sbor  2005  sban  2006  sb3an  2009  sbbi  2010  sbco2h  2015  sbco2d  2017  sbco2vd  2018  sbco3v  2020  sbco3  2025  sbcom2v2  2037  sbcom2  2038  dfsb7  2042  sb7f  2043  sb7af  2044  sbal  2051  sbal1  2053  sbex  2055  sbco4lem  2057  sbco4  2058  sbmo  2137  elsb1  2207  elsb2  2208  eqsb1  2333  clelsb1  2334  clelsb2  2335  cbvabw  2352  clelsb1f  2376  sbabel  2399  sbralie  2783  sbcco  3050  exss  4312  inopab  4851  isarep1  5403  bezoutlemnewy  12503