Theorem sbbii 1709

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

Syntax hints:   <-> wb 184   [wsb 1702

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

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1588  df-sb 1703

This theorem is referenced by:  sbnOLD  2093  sbor  2100  sban  2101  sb3an  2102  sbbi  2103  sbco  2116  sbidm  2119  sbco2d  2123  sbco3  2124  sbco3OLD  2125  equsb3  2146  equsb3ALT  2147  elsb3  2148  elsb4  2149  sbcom4  2162  sb7f  2172  sbex  2185  sbco4lem  2187  sbco4  2188  sbmo  2324  2eu6OLD  2381  eqsb3  2574  clelsb3  2575  cbvab  2595  sbabel  2647  sbralie  3066  sbcco  3317  exss  4666  inopab  5081  isarep1  5608  clelsb3f  26036  2uasbanh  31622  2uasbanhVD  31999  bj-sbnf  32699  bj-clelsb3  32711  bj-sbeq  32755  bj-snsetex  32808