Theorem sbbii 1765

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

Syntax hints:   <-> wb 105   [wsb 1762

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-ial 1534

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

This theorem is referenced by:  sbco2vh  1945  equsb3  1951  sbn  1952  sbim  1953  sbor  1954  sban  1955  sb3an  1958  sbbi  1959  sbco2h  1964  sbco2d  1966  sbco2vd  1967  sbco3v  1969  sbco3  1974  sbcom2v2  1986  sbcom2  1987  dfsb7  1991  sb7f  1992  sb7af  1993  sbal  2000  sbal1  2002  sbex  2004  sbco4lem  2006  sbco4  2007  sbmo  2085  elsb1  2155  elsb2  2156  eqsb1  2281  clelsb1  2282  clelsb2  2283  cbvabw  2300  clelsb1f  2323  sbabel  2346  sbralie  2722  sbcco  2985  exss  4228  inopab  4760  isarep1  5303  bezoutlemnewy  11997