Theorem sbbii 1653

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	⊢ ([y / x]φ ↔ [y / x]ψ)

Proof of Theorem sbbii

Step	Hyp	Ref	Expression
1		sbbii.1	. . . 4 ⊢ (φ ↔ ψ)
2	1	biimpi 186	. . 3 ⊢ (φ → ψ)
3	2	sbimi 1652	. 2 ⊢ ([y / x]φ → [y / x]ψ)
4	1	biimpri 197	. . 3 ⊢ (ψ → φ)
5	4	sbimi 1652	. 2 ⊢ ([y / x]ψ → [y / x]φ)
6	3, 5	impbii 180	1 ⊢ ([y / x]φ ↔ [y / x]ψ)

Syntax hints:   ↔ wb 176  [wsb 1648

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557

This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-sb 1649

This theorem is referenced by:  sbn  2062  sbor  2066  sban  2069  sb3an  2070  sbbi  2071  sbco2d  2087  sbco3  2088  equsb3  2102  elsb3  2103  elsb4  2104  dfsb7  2119  sb7f  2120  sbex  2128  sbmo  2234  2eu6  2289  eqsb3  2454  clelsb3  2455  sbabel  2515  sbralie  2848  sbcco  3068