Metamath Proof Explorer


Theorem pm2.61dan

Description: Elimination of an antecedent. (Contributed by NM, 1-Jan-2005)

Ref Expression
Hypotheses pm2.61dan.1 φ ψ χ
pm2.61dan.2 φ ¬ ψ χ
Assertion pm2.61dan φ χ

Proof

Step Hyp Ref Expression
1 pm2.61dan.1 φ ψ χ
2 pm2.61dan.2 φ ¬ ψ χ
3 1 ex φ ψ χ
4 2 ex φ ¬ ψ χ
5 3 4 pm2.61d φ χ