Metamath Proof Explorer


Theorem bj-cbv3hv2

Description: Version of cbv3h with two disjoint variable conditions, which does not require ax-11 nor ax-13 . (Contributed by BJ, 24-Jun-2019) (Proof modification is discouraged.)

Ref Expression
Hypotheses bj-cbv3hv2.nf ψ x ψ
bj-cbv3hv2.1 x = y φ ψ
Assertion bj-cbv3hv2 x φ y ψ

Proof

Step Hyp Ref Expression
1 bj-cbv3hv2.nf ψ x ψ
2 bj-cbv3hv2.1 x = y φ ψ
3 1 nf5i x ψ
4 3 2 cbv3v2 x φ y ψ