Theorem sbbii 1776

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

Syntax hints:   <-> wb 105   [wsb 1773

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-ial 1545

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

This theorem is referenced by:  sbco2vh  1961  equsb3  1967  sbn  1968  sbim  1969  sbor  1970  sban  1971  sb3an  1974  sbbi  1975  sbco2h  1980  sbco2d  1982  sbco2vd  1983  sbco3v  1985  sbco3  1990  sbcom2v2  2002  sbcom2  2003  dfsb7  2007  sb7f  2008  sb7af  2009  sbal  2016  sbal1  2018  sbex  2020  sbco4lem  2022  sbco4  2023  sbmo  2101  elsb1  2171  elsb2  2172  eqsb1  2297  clelsb1  2298  clelsb2  2299  cbvabw  2316  clelsb1f  2340  sbabel  2363  sbralie  2744  sbcco  3007  exss  4256  inopab  4794  isarep1  5340  bezoutlemnewy  12133