Metamath Proof Explorer


Theorem 19.36v

Description: Version of 19.36 with a disjoint variable condition instead of a nonfreeness hypothesis. (Contributed by NM, 18-Aug-1993) Reduce dependencies on axioms. (Revised by Wolf Lammen, 17-Jan-2020)

Ref Expression
Assertion 19.36v x φ ψ x φ ψ

Proof

Step Hyp Ref Expression
1 19.35 x φ ψ x φ x ψ
2 19.9v x ψ ψ
3 2 imbi2i x φ x ψ x φ ψ
4 1 3 bitri x φ ψ x φ ψ