Metamath Proof Explorer


Theorem bj-exlimmpi

Description: Lemma for bj-vtoclg1f1 (an instance of this lemma is a version of bj-vtoclg1f1 where x and y are identified). (Contributed by BJ, 30-Apr-2019) (Proof modification is discouraged.)

Ref Expression
Hypotheses bj-exlimmpi.nf
|- F/ x ps
bj-exlimmpi.maj
|- ( ch -> ( ph -> ps ) )
bj-exlimmpi.min
|- ph
Assertion bj-exlimmpi
|- ( E. x ch -> ps )

Proof

Step Hyp Ref Expression
1 bj-exlimmpi.nf
 |-  F/ x ps
2 bj-exlimmpi.maj
 |-  ( ch -> ( ph -> ps ) )
3 bj-exlimmpi.min
 |-  ph
4 3 2 mpi
 |-  ( ch -> ps )
5 1 4 exlimi
 |-  ( E. x ch -> ps )