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	|- F/ x ph
	exlimdd.2	|- F/ x ch
	exlimdd.3	|- ( ph -> E. x ps )
	exlimdd.4	|- ( ( ph /\ ps ) -> ch )
Assertion	exlimddOLD	|- ( ph -> ch )

Proof

Step	Hyp	Ref	Expression
1		exlimdd.1	|- F/ x ph
2		exlimdd.2	|- F/ x ch
3		exlimdd.3	|- ( ph -> E. x ps )
4		exlimdd.4	|- ( ( ph /\ ps ) -> ch )
5	4	ex	|- ( ph -> ( ps -> ch ) )
6	1 2 5	exlimd	|- ( ph -> ( E. x ps -> ch ) )
7	3 6	mpd	|- ( ph -> ch )