Metamath Proof Explorer
Description: Existential elimination rule of natural deduction (Rule C, explained in
exlimiv ). (Contributed by Mario Carneiro, 15Jun2016)


Ref 
Expression 

Hypotheses 
exlimddv.1 
⊢ ( 𝜑 → ∃ 𝑥 𝜓 ) 


exlimddv.2 
⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝜒 ) 

Assertion 
exlimddv 
⊢ ( 𝜑 → 𝜒 ) 
Proof
Step 
Hyp 
Ref 
Expression 
1 

exlimddv.1 
⊢ ( 𝜑 → ∃ 𝑥 𝜓 ) 
2 

exlimddv.2 
⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝜒 ) 
3 
2

ex 
⊢ ( 𝜑 → ( 𝜓 → 𝜒 ) ) 
4 
3

exlimdv 
⊢ ( 𝜑 → ( ∃ 𝑥 𝜓 → 𝜒 ) ) 
5 
1 4

mpd 
⊢ ( 𝜑 → 𝜒 ) 