Database
CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY
Predicate calculus with equality: Tarski's system S2 (1 rule, 6 schemes)
Axiom scheme ax-5 (Distinctness) - first use of $d
eximdv
Metamath Proof Explorer
Description: Deduction form of Theorem 19.22 of Margaris p. 90, see exim . See
eximdh and eximd for versions without a distinct variable condition.
(Contributed by NM , 27-Apr-1994)

Ref
Expression
Hypothesis
alimdv.1
$${\u22a2}{\phi}\to \left({\psi}\to {\chi}\right)$$
Assertion
eximdv
$${\u22a2}{\phi}\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}{\psi}\to \exists {x}\phantom{\rule{.4em}{0ex}}{\chi}\right)$$

Proof
Step
Hyp
Ref
Expression
1
alimdv.1
$${\u22a2}{\phi}\to \left({\psi}\to {\chi}\right)$$
2
ax-5
$${\u22a2}{\phi}\to \forall {x}\phantom{\rule{.4em}{0ex}}{\phi}$$
3
2 1
eximdh
$${\u22a2}{\phi}\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}{\psi}\to \exists {x}\phantom{\rule{.4em}{0ex}}{\chi}\right)$$