Metamath Proof Explorer


Theorem exlimiieq2

Description: Inferring a theorem when it is implied by an equality which may be true. (Contributed by BJ, 15-Sep-2018) (Revised by BJ, 30-Sep-2018)

Ref Expression
Hypotheses exlimiieq2.1 𝑦 𝜑
exlimiieq2.2 ( 𝑥 = 𝑦𝜑 )
Assertion exlimiieq2 𝜑

Proof

Step Hyp Ref Expression
1 exlimiieq2.1 𝑦 𝜑
2 exlimiieq2.2 ( 𝑥 = 𝑦𝜑 )
3 ax6er 𝑦 𝑥 = 𝑦
4 1 2 3 exlimii 𝜑