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	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝜓 ) → 𝜒 )
Assertion	r19.29anOLD	⊢ ( ( 𝜑 ∧ ∃ 𝑥 ∈ 𝐴 𝜓 ) → 𝜒 )

Proof

Step	Hyp	Ref	Expression
1		r19.29anOLD.1	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝜓 ) → 𝜒 )
2		nfv	⊢ Ⅎ 𝑥 𝜑
3		nfre1	⊢ Ⅎ 𝑥 ∃ 𝑥 ∈ 𝐴 𝜓
4	2 3	nfan	⊢ Ⅎ 𝑥 ( 𝜑 ∧ ∃ 𝑥 ∈ 𝐴 𝜓 )
5	1	adantllr	⊢ ( ( ( ( 𝜑 ∧ ∃ 𝑥 ∈ 𝐴 𝜓 ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝜓 ) → 𝜒 )
6		simpr	⊢ ( ( 𝜑 ∧ ∃ 𝑥 ∈ 𝐴 𝜓 ) → ∃ 𝑥 ∈ 𝐴 𝜓 )
7	4 5 6	r19.29af	⊢ ( ( 𝜑 ∧ ∃ 𝑥 ∈ 𝐴 𝜓 ) → 𝜒 )