Metamath Proof Explorer


Theorem cbvex4vw

Description: Rule used to change bound variables, using implicit substitution. Version of cbvex4v with more disjoint variable conditions, which requires fewer axioms. (Contributed by NM, 26-Jul-1995) Avoid ax-13 . (Revised by Gino Giotto, 10-Jan-2024)

Ref Expression
Hypotheses cbvex4vw.1 x=vy=uφψ
cbvex4vw.2 z=fw=gψχ
Assertion cbvex4vw xyzwφvufgχ

Proof

Step Hyp Ref Expression
1 cbvex4vw.1 x=vy=uφψ
2 cbvex4vw.2 z=fw=gψχ
3 1 2exbidv x=vy=uzwφzwψ
4 3 cbvex2vw xyzwφvuzwψ
5 2 cbvex2vw zwψfgχ
6 5 2exbii vuzwψvufgχ
7 4 6 bitri xyzwφvufgχ