Theorem cbvald 1702

Description: Deduction used to change bound variables, using implicit substitition, particularly useful in conjunction with dvelim 1743. (The proof was shortened by Andrew Salmon, 25-May-2011.)

Hypotheses

Ref	Expression
cbvald.1	|- (ph -> A.yph)
cbvald.2	|- (ph -> (ps -> A.yps))
cbvald.3	|- (ph -> (x = y -> (ps <-> ch)))

Assertion

Ref	Expression
cbvald	|- (ph -> (A.xps <-> A.ych))

Distinct variable groups:   ph,x   ch,x

Proof of Theorem cbvald

Step	Hyp	Ref	Expression
1		cbvald.1	. 2 |- (ph -> A.yph)
2		ax-17 1317	. . 3 |- (ph -> A.xph)
3	2	hbal 1352	. 2 |- (A.yph -> A.xA.yph)
4		cbvald.2	. . 3 |- (ph -> (ps -> A.yps))
5		ax-17 1317	. . . 4 |- (ch -> A.xch)
6	5	a1i 8	. . 3 |- (ph -> (ch -> A.xch))
7		cbvald.3	. . 3 |- (ph -> (x = y -> (ps <-> ch)))
8	4, 6, 7	cbv2 1524	. 2 |- (A.xA.yph -> (A.xps <-> A.ych))
9	1, 3, 8	3syl 24	1 |- (ph -> (A.xps <-> A.ych))

Syntax hints:   -> wi 3   <-> wb 163  A.wal 1296   = wceq 1298

This theorem is referenced by:  cbvexd 1704  axextnd 6095  axrepndlem1 6096  axunndlem1 6099  axpowndlem2 6102  axpowndlem3 6103  axpowndlem4 6104  axregndlem2 6107  axregnd 6108  axinfndlem1 6109  axinfnd 6110  axacndlem4 6114  axacndlem5 6115  axacnd 6116  axextdist 13866  distel 13870

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-8 1306  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481

This theorem depends on definitions:  df-bi 164  df-an 242

Copyright terms: Public domain