Theorem sbbii 1813

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

Syntax hints:   ↔ wb 105  [wsb 1810

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-ial 1582

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

This theorem is referenced by:  sbco2vh  1998  equsb3  2004  sbn  2005  sbim  2006  sbor  2007  sban  2008  sb3an  2011  sbbi  2012  sbco2h  2017  sbco2d  2019  sbco2vd  2020  sbco3v  2022  sbco3  2027  sbcom2v2  2039  sbcom2  2040  dfsb7  2044  sb7f  2045  sb7af  2046  sbal  2053  sbal1  2055  sbex  2057  sbco4lem  2059  sbco4  2060  sbmo  2139  elsb1  2209  elsb2  2210  eqsb1  2335  clelsb1  2336  clelsb2  2337  cbvabw  2354  clelsb1f  2378  sbabel  2401  sbralie  2785  sbcco  3053  exss  4319  inopab  4862  isarep1  5416  bezoutlemnewy  12566