Theorem sbbii 1538

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	biimpi 168	. . 3 |- (ph -> ps)
3	2	sbimi 1537	. 2 |- ([y / x]ph -> [y / x]ps)
4	1	biimpri 169	. . 3 |- (ps -> ph)
5	4	sbimi 1537	. 2 |- ([y / x]ps -> [y / x]ph)
6	3, 5	impbii 174	1 |- ([y / x]ph <-> [y / x]ps)

Syntax hints:   <-> wb 163  [wsbc 1534

This theorem is referenced by:  sbn 1601  sbor 1605  sban 1607  sb3an 1608  sbbi 1609  sbco2d 1630  sbco3 1631  equsb3 1717  elsb3 1718  elsb3OLD 1719  elsb4 1720  elsb4OLD 1721  dfsb7 1730  sb7f 1731  sbex 1739  sbmo 1796  2eu6 1858  eqsb3 1989  clelsb3 1990  clelsb3OLD 1991  sbabel 2016  sbralie 2453  sbsslem 2978  sbsslemOLD 2979  sbss 2980  brab1 3384  exss 3516  posn 3603  tfinds2 3947  inopab 4108  eqerlem 5328  bnj24 12388  bnj33OLD 12402  bnj38 12409  bnj40 12412  bnj58 12431  bnj62 12433  bnj62OLD 12434  bnj77 12437  bnj77OLD 12438  bnj78 12439  bnj79 12440  bnj79OLD 12441  bnj80 12442  bnj156 12482  bnj220 12511  bnj971 12860  bnj81 13209  bnj82 13210  bnj86 13213  bnj149 13241  bnj154 13245  bnj155 13246  bnj153 13247  bnj581 13294  bnj591 13299  bnj609 13306  bnj1040 13388  bnj1043 13391  bnj1045 13392  bnj1069 13400  bnj1081 13407  bnj1123 13422  bnj1134 13427  sbmoOLD 15654  prtlem5 16245

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-4 1319  ax-5o 1321

This theorem depends on definitions:  df-bi 164  df-an 242  df-ex 1327  df-sb 1536

Copyright terms: Public domain