Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Alan Sare
Conventional Metamath proofs, some derived from VD proofs
eexinst01
Metamath Proof Explorer
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
⊢ ( 𝜑 → 𝜒 )