Theorem sbbii 1753

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 119	. . 3 |- ( ph -> ps )
3	2	sbimi 1752	. 2 |- ( [ y / x ] ph -> [ y / x ] ps )
4	1	biimpri 132	. . 3 |- ( ps -> ph )
5	4	sbimi 1752	. 2 |- ( [ y / x ] ps -> [ y / x ] ph )
6	3, 5	impbii 125	1 |- ( [ y / x ] ph <-> [ y / x ] ps )

Syntax hints:   <-> wb 104   [wsb 1750

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-4 1498  ax-ial 1522

This theorem depends on definitions:  df-bi 116  df-sb 1751

This theorem is referenced by:  sbco2vh  1933  equsb3  1939  sbn  1940  sbim  1941  sbor  1942  sban  1943  sb3an  1946  sbbi  1947  sbco2h  1952  sbco2d  1954  sbco2vd  1955  sbco3v  1957  sbco3  1962  sbcom2v2  1974  sbcom2  1975  dfsb7  1979  sb7f  1980  sb7af  1981  sbal  1988  sbal1  1990  sbex  1992  sbco4lem  1994  sbco4  1995  sbmo  2073  elsb1  2143  elsb2  2144  eqsb1  2270  clelsb1  2271  clelsb2  2272  cbvabw  2289  clelsb1f  2312  sbabel  2335  sbralie  2710  sbcco  2972  exss  4205  inopab  4736  isarep1  5274  bezoutlemnewy  11929