Theorem sbbi 1609

Description: Equivalence inside and outside of a substitution are equivalent.

Assertion

Ref	Expression
sbbi	|- ([y / x](ph <-> ps) <-> ([y / x]ph <-> [y / x]ps))

Proof of Theorem sbbi

Step	Hyp	Ref	Expression
1		dfbi2 572	. . 3 |- ((ph <-> ps) <-> ((ph -> ps) /\ (ps -> ph)))
2	1	sbbii 1538	. 2 |- ([y / x](ph <-> ps) <-> [y / x]((ph -> ps) /\ (ps -> ph)))
3		sbim 1604	. . . 4 |- ([y / x](ph -> ps) <-> ([y / x]ph -> [y / x]ps))
4		sbim 1604	. . . 4 |- ([y / x](ps -> ph) <-> ([y / x]ps -> [y / x]ph))
5	3, 4	anbi12i 540	. . 3 |- (([y / x](ph -> ps) /\ [y / x](ps -> ph)) <-> (([y / x]ph -> [y / x]ps) /\ ([y / x]ps -> [y / x]ph)))
6		sban 1607	. . 3 |- ([y / x]((ph -> ps) /\ (ps -> ph)) <-> ([y / x](ph -> ps) /\ [y / x](ps -> ph)))
7		dfbi2 572	. . 3 |- (([y / x]ph <-> [y / x]ps) <-> (([y / x]ph -> [y / x]ps) /\ ([y / x]ps -> [y / x]ph)))
8	5, 6, 7	3bitr4i 200	. 2 |- ([y / x]((ph -> ps) /\ (ps -> ph)) <-> ([y / x]ph <-> [y / x]ps))
9	2, 8	bitri 190	1 |- ([y / x](ph <-> ps) <-> ([y / x]ph <-> [y / x]ps))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240  [wsbc 1534

This theorem is referenced by:  sblbis 1610  sbrbis 1611  a4sbbi 1616  sbco 1625  sbidm 1627  equsb3lemOLD 1716  elsb3 1718  elsb3OLD 1719  elsb4 1720  elsb4OLD 1721  sbal 1738  sb8eu 1783  eqsb3lemOLD 1988  clelsb3 1990  clelsb3OLD 1991  sbcbidig 2499  sbsslemOLD 2979  pm13.183 16373

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-10 1308  ax-12 1310  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-11o 1588

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

Copyright terms: Public domain