Theorem sbbii 1818

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

Syntax hints:   ↔ wb 105  [wsb 1815

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 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-ial 1587

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

This theorem is referenced by:  sbco2vh  2005  equsb3  2011  sbn  2012  sbim  2013  sbor  2014  sban  2015  sb3an  2018  sbbi  2019  sbco2h  2024  sbco2d  2026  sbco2vd  2027  sbco3v  2029  sbco3  2034  sbcom2v2  2046  sbcom2  2047  dfsb7  2051  sb7f  2052  sb7af  2053  sbal  2060  sbal1  2062  sbex  2064  sbco4lem  2066  sbco4  2067  sbmo  2146  elsb1  2216  elsb2  2217  eqsb1  2342  clelsb1  2343  clelsb2  2344  cbvabw  2363  clelsb1f  2396  sbabel  2419  sbralie  2804  sbcco  3073  exss  4362  inopab  4907  isarep1  5462  bezoutlemnewy  12751