Metamath Proof Explorer


Theorem exlimiieq1

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

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

Proof

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