Theorem exinst01

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	exinst01.1	|- E. x ps
	exinst01.2	|- (. ph ,. ps ->. ch ).
	exinst01.3	|- ( ph -> A. x ph )
	exinst01.4	|- ( ch -> A. x ch )
Assertion	exinst01	|- (. ph ->. ch ).

Proof

Step	Hyp	Ref	Expression
1		exinst01.1	|- E. x ps
2		exinst01.2	|- (. ph ,. ps ->. ch ).
3		exinst01.3	|- ( ph -> A. x ph )
4		exinst01.4	|- ( ch -> A. x ch )
5	2	dfvd2i	|- ( ph -> ( ps -> ch ) )
6	1 5 3 4	eexinst01	|- ( ph -> ch )
7	6	dfvd1ir	|- (. ph ->. ch ).