Theorem cbvex4v 979

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 group(s):   v,u,ph   f,g,ph   x,y,ch   z,w,ch   ps,x,y   ps,f,g   x,z,w,u   y,z,w,v   z,g   w,f

Proof of Theorem cbvex4v

Step	Hyp	Ref	Expression
1		cbvex4v.1	. . . 4 |- ((x = v /\ y = u) -> (ph <-> ps))
2	1	bi2exdv 938	. . 3 |- ((x = v /\ y = u) -> (E.zE.wph <-> E.zE.wps))
3	2	cbvex2v 976	. 2 |- (E.xE.yE.zE.wph <-> E.vE.uE.zE.wps)
4		cbvex4v.2	. . . 4 |- ((z = f /\ w = g) -> (ps <-> ch))
5	4	cbvex2v 976	. . 3 |- (E.zE.wps <-> E.fE.gch)
6	5	bi2ex 734	. 2 |- (E.vE.uE.zE.wps <-> E.vE.uE.fE.gch)
7	3, 6	bitr 151	1 |- (E.xE.yE.zE.wph <-> E.vE.uE.fE.gch)

Syntax hints:   -> wi 2   <-> wb 127   /\ wa 196  E.wex 678   = weq 797

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-12 802  ax-17 925

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679

metamath.org