Theorem sbbii 1718

Description: Infer substitution into both sides of a logical equivalence. (Contributed by NM, 14-May-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 194	. . 3 |- ( ph -> ps )
3	2	sbimi 1717	. 2 |- ( [ y / x ] ph -> [ y / x ] ps )
4	1	biimpri 206	. . 3 |- ( ps -> ph )
5	4	sbimi 1717	. 2 |- ( [ y / x ] ps -> [ y / x ] ph )
6	3, 5	impbii 188	1 |- ( [ y / x ] ph <-> [ y / x ] ps )

Syntax hints:   <-> wb 184   [wsb 1711

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-sb 1712

This theorem is referenced by:  sbnOLD  2106  sbor  2113  sban  2114  sb3an  2115  sbbi  2116  sbco  2129  sbidm  2132  sbco2d  2136  sbco3  2137  sbco3OLD  2138  equsb3  2159  equsb3ALT  2160  elsb3  2161  elsb4  2162  sbcom4  2175  sb7f  2185  sbex  2198  sbco4lem  2200  sbco4  2201  sbmo  2337  2eu6OLD  2394  eqsb3  2587  clelsb3  2588  cbvab  2608  sbabel  2660  sbabelOLD  2661  sbralie  3106  sbcco  3359  exss  4716  inopab  5139  isarep1  5673  clelsb3f  27193  2uasbanh  32770  2uasbanhVD  33147  bj-sbnf  33849  bj-clelsb3  33861  bj-sbeq  33905  bj-snsetex  33958