Theorem r19.29aOLD

Description: Obsolete proof of r19.29a as of 17-Jun-2023. (Contributed by Thierry Arnoux, 22-Nov-2017) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	r19.29aOLD.1	$$⊢\left(\left(\phi \wedge x\in A\right)\wedge \psi \right)\to \chi$$
	r19.29aOLD.2	$$⊢\phi \to \exists x\in A\psi$$
Assertion	r19.29aOLD	$$⊢\phi \to \chi$$

Proof

Step	Hyp	Ref	Expression
1		r19.29aOLD.1	$$⊢\left(\left(\phi \wedge x\in A\right)\wedge \psi \right)\to \chi$$
2		r19.29aOLD.2	$$⊢\phi \to \exists x\in A\psi$$
3		nfv	$$⊢Ⅎx\phi$$
4	3 1 2	r19.29af	$$⊢\phi \to \chi$$