Metamath Proof Explorer


Theorem 19.45v

Description: Version of 19.45 with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 12-Mar-1993)

Ref Expression
Assertion 19.45v x φ ψ φ x ψ

Proof

Step Hyp Ref Expression
1 19.43 x φ ψ x φ x ψ
2 19.9v x φ φ
3 2 orbi1i x φ x ψ φ x ψ
4 1 3 bitri x φ ψ φ x ψ