Theorem cbvald 1319

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

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 1102	. . . 4 |- ((ph -> ps) -> A.y(ph -> ps))
4		ax-17 970	. . . 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 584	. . . 4 |- (x = y -> ((ph -> ps) <-> (ph -> ch)))
8	3, 4, 7	cbval 1164	. . 3 |- (A.x(ph -> ps) <-> A.y(ph -> ch))
9		19.21v 1284	. . 3 |- (A.x(ph -> ps) <-> (ph -> A.xps))
10	1	19.21 1055	. . 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 586	1 |- (ph -> (A.xps <-> A.ych))

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

This theorem is referenced by:  cbvexd 1320  axextnd 4926  axrepndlem1 4927  axunndlem1 4930  axpowndlem2 4933  axpowndlem3 4934  axpowndlem4 4935  axregndlem2 4938  axregnd 4939  axinfndlem1 4940  axinfnd 4941  axacndlem4 4945  axacndlem5 4946  axacnd 4947

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-12 967  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122

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

Copyright terms: Public domain