Metamath Proof Explorer


Theorem cbval2vw

Description: Version of cbval2vv with more disjoint variable conditions, which requires fewer axioms . (Contributed by Gino Giotto, 10-Jan-2024)

Ref Expression
Hypothesis cbval2vw.1 x = z y = w φ ψ
Assertion cbval2vw x y φ z w ψ

Proof

Step Hyp Ref Expression
1 cbval2vw.1 x = z y = w φ ψ
2 1 cbvaldvaw x = z y φ w ψ
3 2 cbvalvw x y φ z w ψ