Theorem r19.29anOLD

Description: Obsolete version of r19.29an as of 17-Jun-2023. (Contributed by Thierry Arnoux, 29-Dec-2019) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		r19.29anOLD.1	$$⊢\left(\left(\phi \wedge x\in A\right)\wedge \psi \right)\to \chi$$
2		nfv	$$⊢Ⅎx\phi$$
3		nfre1	$$⊢Ⅎx\exists x\in A\psi$$
4	2 3	nfan	$$⊢Ⅎx\left(\phi \wedge \exists x\in A\psi \right)$$
5	1	adantllr	$$⊢\left(\left(\left(\phi \wedge \exists x\in A\psi \right)\wedge x\in A\right)\wedge \psi \right)\to \chi$$
6		simpr	$$⊢\left(\phi \wedge \exists x\in A\psi \right)\to \exists x\in A\psi$$
7	4 5 6	r19.29af	$$⊢\left(\phi \wedge \exists x\in A\psi \right)\to \chi$$