Metamath Proof Explorer


Theorem bj-cbvex4vv

Description: Version of cbvex4v with a disjoint variable condition, which does not require ax-13 . (Contributed by BJ, 16-Jun-2019) (Proof modification is discouraged.)

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

Proof

Step Hyp Ref Expression
1 bj-cbvex4vv.1 x=vy=uφψ
2 bj-cbvex4vv.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χ