Theorem sbbii 1688

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

Syntax hints:   <-> wb 103   [wsb 1685

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-4 1440  ax-ial 1467

This theorem depends on definitions:  df-bi 115  df-sb 1686

This theorem is referenced by:  sbco2v  1862  equsb3  1866  sbn  1867  sbim  1868  sbor  1869  sban  1870  sb3an  1873  sbbi  1874  sbco2h  1879  sbco2d  1881  sbco2vd  1882  sbco3v  1884  sbco3  1889  elsb3  1893  elsb4  1894  sbcom2v2  1903  sbcom2  1904  dfsb7  1908  sb7f  1909  sb7af  1910  sbal  1917  sbal1  1919  sbex  1921  sbco4lem  1923  sbco4  1924  sbmo  2000  eqsb3  2182  clelsb3  2183  clelsb4  2184  sbabel  2244  sbralie  2590  sbcco  2836  exss  3982  inopab  4486  isarep1  5005  bezoutlemnewy  10385