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 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 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  2355  clelsb1f  2379  sbabel  2402  sbralie  2786  sbcco  3054  exss  4325  inopab  4868  isarep1  5423  bezoutlemnewy  12630