Theorem sbbii 1779

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

Syntax hints:   <-> wb 105   [wsb 1776

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-ial 1548

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

This theorem is referenced by:  sbco2vh  1964  equsb3  1970  sbn  1971  sbim  1972  sbor  1973  sban  1974  sb3an  1977  sbbi  1978  sbco2h  1983  sbco2d  1985  sbco2vd  1986  sbco3v  1988  sbco3  1993  sbcom2v2  2005  sbcom2  2006  dfsb7  2010  sb7f  2011  sb7af  2012  sbal  2019  sbal1  2021  sbex  2023  sbco4lem  2025  sbco4  2026  sbmo  2104  elsb1  2174  elsb2  2175  eqsb1  2300  clelsb1  2301  clelsb2  2302  cbvabw  2319  clelsb1f  2343  sbabel  2366  sbralie  2747  sbcco  3011  exss  4260  inopab  4798  isarep1  5344  bezoutlemnewy  12163