Theorem sbbii 1170

Description: Infer substitution into both sides of a logical equivalence.

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	biimp 151	. . 3 |- (ph -> ps)
3	2	sbimi 1169	. 2 |- ([y / x]ph -> [y / x]ps)
4	1	biimpr 152	. . 3 |- (ps -> ph)
5	4	sbimi 1169	. 2 |- ([y / x]ps -> [y / x]ph)
6	3, 5	impbi 157	1 |- ([y / x]ph <-> [y / x]ps)

Syntax hints:   <-> wb 146  [wsbc 1166

This theorem is referenced by:  sbn 1226  sbor 1230  sban 1232  sb3an 1233  sbbi 1234  sbco2d 1251  sbco3 1252  equsb3 1325  elsb3 1326  dfsb7 1335  sbex 1343  2eu6 1447  sbabel 1576  sbralie 1931  exss 2759  tfinds2 3155  inopab 3258  eqerlem 4254

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-4 970  ax-5o 972

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978  df-sb 1168

Copyright terms: Public domain