Theorem sbbii 1738

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

Syntax hints:   <-> wb 104   [wsb 1735

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 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-ial 1514

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

This theorem is referenced by:  sbco2vh  1918  equsb3  1924  sbn  1925  sbim  1926  sbor  1927  sban  1928  sb3an  1931  sbbi  1932  sbco2h  1937  sbco2d  1939  sbco2vd  1940  sbco3v  1942  sbco3  1947  elsb3  1951  elsb4  1952  sbcom2v2  1961  sbcom2  1962  dfsb7  1966  sb7f  1967  sb7af  1968  sbal  1975  sbal1  1977  sbex  1979  sbco4lem  1981  sbco4  1982  sbmo  2058  eqsb3  2243  clelsb3  2244  clelsb4  2245  cbvabw  2262  clelsb3f  2285  sbabel  2307  sbralie  2670  sbcco  2930  exss  4149  inopab  4671  isarep1  5209  bezoutlemnewy  11684