Metamath Proof Explorer


Theorem bj-cbvexdv

Description: Version of cbvexd 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-cbvaldv.1 y φ
bj-cbvaldv.2 φ y ψ
bj-cbvaldv.3 φ x = y ψ χ
Assertion bj-cbvexdv φ x ψ y χ

Proof

Step Hyp Ref Expression
1 bj-cbvaldv.1 y φ
2 bj-cbvaldv.2 φ y ψ
3 bj-cbvaldv.3 φ x = y ψ χ
4 2 nfnd φ y ¬ ψ
5 notbi ψ χ ¬ ψ ¬ χ
6 3 5 syl6ib φ x = y ¬ ψ ¬ χ
7 1 4 6 bj-cbvaldv φ x ¬ ψ y ¬ χ
8 7 notbid φ ¬ x ¬ ψ ¬ y ¬ χ
9 df-ex x ψ ¬ x ¬ ψ
10 df-ex y χ ¬ y ¬ χ
11 8 9 10 3bitr4g φ x ψ y χ