Theorem sbbii 1733

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

Syntax hints:   <-> wb 184   [wsb 1726

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

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1600  df-sb 1727

This theorem is referenced by:  sbor  2125  sban  2126  sb3an  2127  sbbi  2128  sbco  2140  sbidm  2142  sbco2d  2145  sbco3  2146  equsb3  2162  equsb3ALT  2163  elsb3  2164  elsb4  2165  sbcom4  2176  sb7f  2183  sbex  2193  sbco4lem  2195  sbco4  2196  sbmo  2321  2eu6OLD  2370  eqsb3  2563  clelsb3  2564  cbvab  2584  sbabel  2636  sbabelOLD  2637  sbralie  3083  sbcco  3336  exss  4700  inopab  5123  isarep1  5657  clelsb3f  27357  2uasbanh  33202  2uasbanhVD  33579  bj-sbnf  34295  bj-clelsb3  34307  bj-sbeq  34351  bj-snsetex  34404  frege72  37767