Metamath Proof Explorer

Theorem 19.42v

Description: Version of 19.42 with a disjoint variable condition requiring fewer axioms. (Contributed by NM, 21-Jun-1993)

Ref Expression
Assertion 19.42v x φ ψ φ x ψ


Step Hyp Ref Expression
1 19.41v x ψ φ x ψ φ
2 exancom x φ ψ x ψ φ
3 ancom φ x ψ x ψ φ
4 1 2 3 3bitr4i x φ ψ φ x ψ