Theorem sbbii 1648

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

Syntax hints:   <-> wb 98   [wsb 1645

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-ial 1427

This theorem depends on definitions:  df-bi 110  df-sb 1646

This theorem is referenced by:  sbco2v  1821  equsb3  1825  sbn  1826  sbim  1827  sbor  1828  sban  1829  sb3an  1832  sbbi  1833  sbco2h  1838  sbco2d  1840  sbco2vd  1841  sbco3v  1843  sbco3  1848  elsb3  1852  elsb4  1853  sbcom2v2  1862  sbcom2  1863  dfsb7  1867  sb7f  1868  sb7af  1869  sbal  1876  sbal1  1878  sbex  1880  sbco4lem  1882  sbco4  1883  sbmo  1959  eqsb3  2141  clelsb3  2142  clelsb4  2143  sbabel  2203  sbralie  2546  sbcco  2785  exss  3963  inopab  4468  isarep1  4985