Theorem exlimddvfi

Description: A lemma for eliminating an existential quantifier, in inference form. (Contributed by Giovanni Mascellani, 31-May-2019)

	Ref	Expression
Hypotheses	exlimddvfi.1	⊢ ( 𝜑 → ∃ 𝑥 𝜃 )
	exlimddvfi.2	⊢ Ⅎ 𝑦 𝜃
	exlimddvfi.3	⊢ Ⅎ 𝑦 𝜓
	exlimddvfi.4	⊢ ( [ 𝑦 / 𝑥 ] 𝜃 ↔ 𝜂 )
	exlimddvfi.5	⊢ ( ( 𝜂 ∧ 𝜓 ) → 𝜒 )
	exlimddvfi.6	⊢ Ⅎ 𝑦 𝜒
Assertion	exlimddvfi	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝜒 )

Proof

Step	Hyp	Ref	Expression
1		exlimddvfi.1	⊢ ( 𝜑 → ∃ 𝑥 𝜃 )
2		exlimddvfi.2	⊢ Ⅎ 𝑦 𝜃
3		exlimddvfi.3	⊢ Ⅎ 𝑦 𝜓
4		exlimddvfi.4	⊢ ( [ 𝑦 / 𝑥 ] 𝜃 ↔ 𝜂 )
5		exlimddvfi.5	⊢ ( ( 𝜂 ∧ 𝜓 ) → 𝜒 )
6		exlimddvfi.6	⊢ Ⅎ 𝑦 𝜒
7	2	sb8e	⊢ ( ∃ 𝑥 𝜃 ↔ ∃ 𝑦 [ 𝑦 / 𝑥 ] 𝜃 )
8	1 7	sylib	⊢ ( 𝜑 → ∃ 𝑦 [ 𝑦 / 𝑥 ] 𝜃 )
9		sbsbc	⊢ ( [ 𝑦 / 𝑥 ] 𝜃 ↔ [ 𝑦 / 𝑥 ] 𝜃 )
10	9 4	bitri	⊢ ( [ 𝑦 / 𝑥 ] 𝜃 ↔ 𝜂 )
11	10 5	sylanb	⊢ ( ( [ 𝑦 / 𝑥 ] 𝜃 ∧ 𝜓 ) → 𝜒 )
12	8 3 11 6	exlimddvf	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝜒 )