Metamath Proof Explorer


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 (    𝜑    ▶    𝜒    )