Metamath Proof Explorer


Theorem eexinst01

Description: exinst01 without virtual deductions. (Contributed by Alan Sare, 21-Apr-2013) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses eexinst01.1 x ψ
eexinst01.2 φ ψ χ
eexinst01.3 φ x φ
eexinst01.4 χ x χ
Assertion eexinst01 φ χ

Proof

Step Hyp Ref Expression
1 eexinst01.1 x ψ
2 eexinst01.2 φ ψ χ
3 eexinst01.3 φ x φ
4 eexinst01.4 χ x χ
5 3 4 2 exlimdh φ x ψ χ
6 1 5 mpi φ χ