Theorem sbbii 1814

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

Syntax hints:   ↔ wb 105  [wsb 1811

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-ial 1583

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

This theorem is referenced by:  sbco2vh  2001  equsb3  2007  sbn  2008  sbim  2009  sbor  2010  sban  2011  sb3an  2014  sbbi  2015  sbco2h  2020  sbco2d  2022  sbco2vd  2023  sbco3v  2025  sbco3  2030  sbcom2v2  2042  sbcom2  2043  dfsb7  2047  sb7f  2048  sb7af  2049  sbal  2056  sbal1  2058  sbex  2060  sbco4lem  2062  sbco4  2063  sbmo  2142  elsb1  2212  elsb2  2213  eqsb1  2338  clelsb1  2339  clelsb2  2340  cbvabw  2359  clelsb1f  2390  sbabel  2413  sbralie  2798  sbcco  3067  exss  4348  inopab  4892  isarep1  5447  bezoutlemnewy  12717