Theorem sbbii 1758

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

Syntax hints:   <-> wb 104   [wsb 1755

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-ial 1527

This theorem depends on definitions:  df-bi 116  df-sb 1756

This theorem is referenced by:  sbco2vh  1938  equsb3  1944  sbn  1945  sbim  1946  sbor  1947  sban  1948  sb3an  1951  sbbi  1952  sbco2h  1957  sbco2d  1959  sbco2vd  1960  sbco3v  1962  sbco3  1967  sbcom2v2  1979  sbcom2  1980  dfsb7  1984  sb7f  1985  sb7af  1986  sbal  1993  sbal1  1995  sbex  1997  sbco4lem  1999  sbco4  2000  sbmo  2078  elsb1  2148  elsb2  2149  eqsb1  2274  clelsb1  2275  clelsb2  2276  cbvabw  2293  clelsb1f  2316  sbabel  2339  sbralie  2714  sbcco  2976  exss  4212  inopab  4743  isarep1  5284  bezoutlemnewy  11951