Theorem sbbii 1789

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

Syntax hints:   <-> wb 105   [wsb 1786

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-ial 1558

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

This theorem is referenced by:  sbco2vh  1974  equsb3  1980  sbn  1981  sbim  1982  sbor  1983  sban  1984  sb3an  1987  sbbi  1988  sbco2h  1993  sbco2d  1995  sbco2vd  1996  sbco3v  1998  sbco3  2003  sbcom2v2  2015  sbcom2  2016  dfsb7  2020  sb7f  2021  sb7af  2022  sbal  2029  sbal1  2031  sbex  2033  sbco4lem  2035  sbco4  2036  sbmo  2115  elsb1  2185  elsb2  2186  eqsb1  2311  clelsb1  2312  clelsb2  2313  cbvabw  2330  clelsb1f  2354  sbabel  2377  sbralie  2760  sbcco  3027  exss  4289  inopab  4828  isarep1  5379  bezoutlemnewy  12432