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
⊢ ∃ 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
⊢ φ → χ