Theorem exlimddOLD

Description: Obsolete version of exlimdd as of 3-Sep-2023. (Contributed by Mario Carneiro, 9-Feb-2017) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	exlimdd.1	$$⊢Ⅎx\phi$$
	exlimdd.2	$$⊢Ⅎx\chi$$
	exlimdd.3	$$⊢\phi \to \exists x\psi$$
	exlimdd.4	$$⊢\left(\phi \wedge \psi \right)\to \chi$$
Assertion	exlimddOLD	$$⊢\phi \to \chi$$

Proof

Step	Hyp	Ref	Expression
1		exlimdd.1	$$⊢Ⅎx\phi$$
2		exlimdd.2	$$⊢Ⅎx\chi$$
3		exlimdd.3	$$⊢\phi \to \exists x\psi$$
4		exlimdd.4	$$⊢\left(\phi \wedge \psi \right)\to \chi$$
5	4	ex	$$⊢\phi \to \left(\psi \to \chi \right)$$
6	1 2 5	exlimd	$$⊢\phi \to \left(\exists x\psi \to \chi \right)$$
7	3 6	mpd	$$⊢\phi \to \chi$$