Theorem sbbii 1788

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

Syntax hints:   <-> wb 105   [wsb 1785

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-ial 1557

This theorem depends on definitions:  df-bi 117  df-sb 1786

This theorem is referenced by:  sbco2vh  1973  equsb3  1979  sbn  1980  sbim  1981  sbor  1982  sban  1983  sb3an  1986  sbbi  1987  sbco2h  1992  sbco2d  1994  sbco2vd  1995  sbco3v  1997  sbco3  2002  sbcom2v2  2014  sbcom2  2015  dfsb7  2019  sb7f  2020  sb7af  2021  sbal  2028  sbal1  2030  sbex  2032  sbco4lem  2034  sbco4  2035  sbmo  2113  elsb1  2183  elsb2  2184  eqsb1  2309  clelsb1  2310  clelsb2  2311  cbvabw  2328  clelsb1f  2352  sbabel  2375  sbralie  2756  sbcco  3020  exss  4271  inopab  4810  isarep1  5360  bezoutlemnewy  12317