Theorem sbbii 1745

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

Syntax hints:   <-> wb 104   [wsb 1742

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 1427  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-4 1490  ax-ial 1514

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

This theorem is referenced by:  sbco2vh  1925  equsb3  1931  sbn  1932  sbim  1933  sbor  1934  sban  1935  sb3an  1938  sbbi  1939  sbco2h  1944  sbco2d  1946  sbco2vd  1947  sbco3v  1949  sbco3  1954  sbcom2v2  1966  sbcom2  1967  dfsb7  1971  sb7f  1972  sb7af  1973  sbal  1980  sbal1  1982  sbex  1984  sbco4lem  1986  sbco4  1987  sbmo  2065  elsb3  2135  elsb4  2136  eqsb3  2261  clelsb3  2262  clelsb4  2263  cbvabw  2280  clelsb3f  2303  sbabel  2326  sbralie  2696  sbcco  2958  exss  4187  inopab  4718  isarep1  5256  bezoutlemnewy  11880