Theorem cbvald 1315

Description: Deduction used to change bound variables with implicit substitution, particularly useful in conjunction with dvelim 1347.

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	. . . . 5 |- (ph -> A.yph)
2		cbvald.2	. . . . 5 |- (ph -> (ps -> A.yps))
3	1, 2	hbim1 1099	. . . 4 |- ((ph -> ps) -> A.y(ph -> ps))
4		ax-17 968	. . . 4 |- ((ph -> ch) -> A.x(ph -> ch))
5		cbvald.3	. . . . . 6 |- (ph -> (x = y -> (ps <-> ch)))
6	5	com12 11	. . . . 5 |- (x = y -> (ph -> (ps <-> ch)))
7	6	pm5.74d 583	. . . 4 |- (x = y -> ((ph -> ps) <-> (ph -> ch)))
8	3, 4, 7	cbval 1161	. . 3 |- (A.x(ph -> ps) <-> A.y(ph -> ch))
9		19.21v 1280	. . 3 |- (A.x(ph -> ps) <-> (ph -> A.xps))
10	1	19.21 1052	. . 3 |- (A.y(ph -> ch) <-> (ph -> A.ych))
11	8, 9, 10	3bitr3 181	. 2 |- ((ph -> A.xps) <-> (ph -> A.ych))
12	11	pm5.74ri 585	1 |- (ph -> (A.xps <-> A.ych))

Syntax hints:   -> wi 3   <-> wb 146  A.wal 951   = wceq 953

This theorem is referenced by:  cbvexd 1316  axextnd 4915  axrepndlem1 4916  axunndlem1 4919  axpowndlem2 4922  axpowndlem3 4923  axpowndlem4 4924  axregndlem2 4927  axregnd 4928  axinfndlem1 4929  axinfnd 4930  axacndlem4 4934  axacndlem5 4935  axacnd 4936

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain