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
|- F/ x ph
exlimiieq1.2
|- ( x = y -> ph )
Assertion exlimiieq1
|- ph

Proof

Step Hyp Ref Expression
1 exlimiieq1.1
 |-  F/ x ph
2 exlimiieq1.2
 |-  ( x = y -> ph )
3 ax6e
 |-  E. x x = y
4 1 2 3 exlimii
 |-  ph