Metamath Proof Explorer


Theorem cbvexd

Description: Deduction used to change bound variables, using implicit substitution, particularly useful in conjunction with dvelim . Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker cbvexdw if possible. (Contributed by NM, 2-Jan-2002) (Revised by Mario Carneiro, 6-Oct-2016) (New usage is discouraged.)

Ref Expression
Hypotheses cbvald.1 y φ
cbvald.2 φ y ψ
cbvald.3 φ x = y ψ χ
Assertion cbvexd φ x ψ y χ

Proof

Step Hyp Ref Expression
1 cbvald.1 y φ
2 cbvald.2 φ y ψ
3 cbvald.3 φ x = y ψ χ
4 2 nfnd φ y ¬ ψ
5 notbi ψ χ ¬ ψ ¬ χ
6 3 5 syl6ib φ x = y ¬ ψ ¬ χ
7 1 4 6 cbvald φ x ¬ ψ y ¬ χ
8 alnex x ¬ ψ ¬ x ψ
9 alnex y ¬ χ ¬ y χ
10 7 8 9 3bitr3g φ ¬ x ψ ¬ y χ
11 10 con4bid φ x ψ y χ