Theorem sbbii 1172

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

Syntax hints:   <-> wb 146  [wsbc 1168

This theorem is referenced by:  sbn 1229  sbor 1233  sban 1235  sb3an 1236  sbbi 1237  sbco2d 1254  sbco3 1255  equsb3 1328  elsb3 1329  dfsb7 1338  sbex 1346  2eu6 1452  sbabel 1581  sbralie 1937  exss 2764  tfinds2 3160  inopab 3263  eqerlem 4260

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 961  ax-4 971  ax-5o 973

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-sb 1170

Copyright terms: Public domain