Theorem sbf3t 1619

Description: Substitution has no effect on a non-free variable.

Assertion

Ref	Expression
sbf3t	|- (A.x(ph -> A.xph) -> ([y / x]ph <-> ph))

Proof of Theorem sbf3t

Step	Hyp	Ref	Expression
1		a4sbim 1614	. . 3 |- (A.x(ph -> A.xph) -> ([y / x]ph -> [y / x]A.xph))
2		sbf2 1552	. . . 4 |- ([y / x]A.xph <-> A.xph)
3		ax-4 1319	. . . 4 |- (A.xph -> ph)
4	2, 3	sylbi 216	. . 3 |- ([y / x]A.xph -> ph)
5	1, 4	syl6 25	. 2 |- (A.x(ph -> A.xph) -> ([y / x]ph -> ph))
6		stdpc4 1550	. . . 4 |- (A.xph -> [y / x]ph)
7	6	imim2i 11	. . 3 |- ((ph -> A.xph) -> (ph -> [y / x]ph))
8	7	a4s 1330	. 2 |- (A.x(ph -> A.xph) -> (ph -> [y / x]ph))
9	5, 8	impbid 574	1 |- (A.x(ph -> A.xph) -> ([y / x]ph <-> ph))

Syntax hints:   -> wi 3   <-> wb 163  A.wal 1296  [wsbc 1534

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