Theorem cbvex4v 1320

Description: Rule used to change bound variables with implicit substitution.

Hypotheses

Ref	Expression
cbvex4v.1	|- ((x = v /\ y = u) -> (ph <-> ps))
cbvex4v.2	|- ((z = f /\ w = g) -> (ps <-> ch))

Assertion

Ref	Expression
cbvex4v	|- (E.xE.yE.zE.wph <-> E.vE.uE.fE.gch)

Distinct variable groups:   z,w,ch   v,u,ph   x,y,ps   f,g,ps   w,f   z,g   w,u,x,y,z,v

Proof of Theorem cbvex4v

Step	Hyp	Ref	Expression
1		cbvex4v.1	. . . 4 |- ((x = v /\ y = u) -> (ph <-> ps))
2	1	2exbidv 1279	. . 3 |- ((x = v /\ y = u) -> (E.zE.wph <-> E.zE.wps))
3	2	cbvex2v 1317	. 2 |- (E.xE.yE.zE.wph <-> E.vE.uE.zE.wps)
4		cbvex4v.2	. . . 4 |- ((z = f /\ w = g) -> (ps <-> ch))
5	4	cbvex2v 1317	. . 3 |- (E.zE.wps <-> E.fE.gch)
6	5	2exbii 1050	. 2 |- (E.vE.uE.zE.wps <-> E.vE.uE.fE.gch)
7	3, 6	bitr 173	1 |- (E.xE.yE.zE.wph <-> E.vE.uE.fE.gch)

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223   = wceq 954  E.wex 978

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 979

Copyright terms: Public domain