Theorem cbvald 1322

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

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 1105	. . . 4 |- ((ph -> ps) -> A.y(ph -> ps))
4		ax-17 973	. . . 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 587	. . . 4 |- (x = y -> ((ph -> ps) <-> (ph -> ch)))
8	3, 4, 7	cbval 1167	. . 3 |- (A.x(ph -> ps) <-> A.y(ph -> ch))
9		19.21v 1287	. . 3 |- (A.x(ph -> ps) <-> (ph -> A.xps))
10	1	19.21 1058	. . 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 589	1 |- (ph -> (A.xps <-> A.ych))

Syntax hints:   -> wi 3   <-> wb 146  A.wal 956   = wceq 958

This theorem is referenced by:  cbvexd 1323  axextnd 4962  axrepndlem1 4963  axunndlem1 4966  axpowndlem2 4969  axpowndlem3 4970  axpowndlem4 4971  axregndlem2 4974  axregnd 4975  axinfndlem1 4976  axinfnd 4977  axacndlem4 4981  axacndlem5 4982  axacnd 4983

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125

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

Copyright terms: Public domain