Metamath Proof Explorer


Theorem ceqsexv2dOLD

Description: Obsolete version of ceqsexv2d as of 5-Jun-2025. (Contributed by Thierry Arnoux, 10-Sep-2016) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses ceqsexv2dOLD.1 A V
ceqsexv2dOLD.2 x = A φ ψ
ceqsexv2dOLD.3 ψ
Assertion ceqsexv2dOLD x φ

Proof

Step Hyp Ref Expression
1 ceqsexv2dOLD.1 A V
2 ceqsexv2dOLD.2 x = A φ ψ
3 ceqsexv2dOLD.3 ψ
4 1 2 ceqsexv x x = A φ ψ
5 4 biimpri ψ x x = A φ
6 exsimpr x x = A φ x φ
7 3 5 6 mp2b x φ