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 𝑥 𝜓
eexinst01.2 ( 𝜑 → ( 𝜓𝜒 ) )
eexinst01.3 ( 𝜑 → ∀ 𝑥 𝜑 )
eexinst01.4 ( 𝜒 → ∀ 𝑥 𝜒 )
Assertion eexinst01 ( 𝜑𝜒 )

Proof

Step Hyp Ref Expression
1 eexinst01.1 𝑥 𝜓
2 eexinst01.2 ( 𝜑 → ( 𝜓𝜒 ) )
3 eexinst01.3 ( 𝜑 → ∀ 𝑥 𝜑 )
4 eexinst01.4 ( 𝜒 → ∀ 𝑥 𝜒 )
5 3 4 2 exlimdh ( 𝜑 → ( ∃ 𝑥 𝜓𝜒 ) )
6 1 5 mpi ( 𝜑𝜒 )