Metamath Proof Explorer


Theorem opnneirv

Description: A variant of opnneir with different dummy variables. (Contributed by Zhi Wang, 31-Aug-2024)

Ref Expression
Hypotheses opnneir.1 φ J Top
opnneirv.2 φ x = y ψ χ
Assertion opnneirv φ x J S x ψ y nei J S χ

Proof

Step Hyp Ref Expression
1 opnneir.1 φ J Top
2 opnneirv.2 φ x = y ψ χ
3 2 opnneilem φ x J S x ψ y J S y χ
4 1 opnneir φ y J S y χ y nei J S χ
5 3 4 sylbid φ x J S x ψ y nei J S χ