Theorem r19.41dv

Description: A complex deduction form of r19.41v . (Contributed by Zhi Wang, 6-Sep-2024)

	Ref	Expression
Hypothesis	r19.41dv.1	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 𝜓 )
Assertion	r19.41dv	⊢ ( ( 𝜑 ∧ 𝜒 ) → ∃ 𝑥 ∈ 𝐴 ( 𝜓 ∧ 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		r19.41dv.1	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 𝜓 )
2	1	anim1i	⊢ ( ( 𝜑 ∧ 𝜒 ) → ( ∃ 𝑥 ∈ 𝐴 𝜓 ∧ 𝜒 ) )
3		r19.41v	⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝜓 ∧ 𝜒 ) ↔ ( ∃ 𝑥 ∈ 𝐴 𝜓 ∧ 𝜒 ) )
4	2 3	sylibr	⊢ ( ( 𝜑 ∧ 𝜒 ) → ∃ 𝑥 ∈ 𝐴 ( 𝜓 ∧ 𝜒 ) )