Metamath Proof Explorer


Theorem negel

Description: An inference for negation elimination. (Contributed by Giovanni Mascellani, 24-May-2019)

Ref Expression
Hypotheses negel.1 ψ χ
negel.2 φ ¬ χ
Assertion negel φ ψ

Proof

Step Hyp Ref Expression
1 negel.1 ψ χ
2 negel.2 φ ¬ χ
3 1 adantl φ ψ χ
4 2 adantr φ ψ ¬ χ
5 3 4 pm2.21fal φ ψ