Theorem sbbii 1653

Description: Infer substitution into both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
sbbii.1	|- (ph <-> ps)

Assertion

Ref	Expression
sbbii	|- ([y / x]ph <-> [y / x]ps)

Proof of Theorem sbbii

Step	Hyp	Ref	Expression
1		sbbii.1	. . . 4 |- (ph <-> ps)
2	1	biimpi 186	. . 3 |- (ph -> ps)
3	2	sbimi 1652	. 2 |- ([y / x]ph -> [y / x]ps)
4	1	biimpri 197	. . 3 |- (ps -> ph)
5	4	sbimi 1652	. 2 |- ([y / x]ps -> [y / x]ph)
6	3, 5	impbii 180	1 |- ([y / x]ph <-> [y / x]ps)

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  elsb1  2103  elsb2  2104  dfsb7  2119  sb7f  2120  sbex  2128  sbmo  2234  2eu6  2289  eqsb1  2454  clelsb1  2455  clelsb2  2456  sbabel  2516  sbralie  2849  sbcco  3069