Theorem exinst11

Description: Existential Instantiation. Virtual Deduction rule corresponding to a special case of the Natural Deduction Sequent Calculus rule called Rule C in Margaris p. 79 and E E. in Table 1 on page 4 of the paper "Extracting information from intermediate T-systems" (2000) presented at IMLA99 by Mauro Ferrari, Camillo Fiorentini, and Pierangelo Miglioli. (Contributed by Alan Sare, 21-Apr-2013) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	exinst11.1	⊢ (    𝜑    ▶    ∃ 𝑥 𝜓    )
	exinst11.2	⊢ (    𝜑    ,    𝜓    ▶    𝜒    )
	exinst11.3	⊢ ( 𝜑 → ∀ 𝑥 𝜑 )
	exinst11.4	⊢ ( 𝜒 → ∀ 𝑥 𝜒 )
Assertion	exinst11	⊢ (    𝜑    ▶    𝜒    )

Proof

Step	Hyp	Ref	Expression
1		exinst11.1	⊢ (    𝜑    ▶    ∃ 𝑥 𝜓    )
2		exinst11.2	⊢ (    𝜑    ,    𝜓    ▶    𝜒    )
3		exinst11.3	⊢ ( 𝜑 → ∀ 𝑥 𝜑 )
4		exinst11.4	⊢ ( 𝜒 → ∀ 𝑥 𝜒 )
5	1	in1	⊢ ( 𝜑 → ∃ 𝑥 𝜓 )
6	2	dfvd2i	⊢ ( 𝜑 → ( 𝜓 → 𝜒 ) )
7	5 6 3 4	eexinst11	⊢ ( 𝜑 → 𝜒 )
8	7	dfvd1ir	⊢ (    𝜑    ▶    𝜒    )