Theorem exanOLD

Description: Obsolete proof of exan as of 19-Jun-2023. (Contributed by NM, 18-Aug-1993) (Proof shortened by Andrew Salmon, 25-May-2011) (Proof shortened by Wolf Lammen, 13-Jan-2018) Reduce axiom dependencies. (Revised by BJ, 7-Jul-2021) (Proof shortened by Wolf Lammen, 6-Nov-2022) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypothesis	exanOLD.1	$$⊢\left(\exists x\phi \wedge \psi \right)$$
Assertion	exanOLD	$$⊢\exists x\left(\phi \wedge \psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		exanOLD.1	$$⊢\left(\exists x\phi \wedge \psi \right)$$
2	1	simpli	$$⊢\exists x\phi$$
3	1	simpri	$$⊢\psi$$
4	3	jctr	$$⊢\phi \to \left(\phi \wedge \psi \right)$$
5	2 4	eximii	$$⊢\exists x\left(\phi \wedge \psi \right)$$