Metamath Proof Explorer


Theorem 4cases

Description: Inference eliminating two antecedents from the four possible cases that result from their true/false combinations. (Contributed by NM, 25-Oct-2003)

Ref Expression
Hypotheses 4cases.1 φ ψ χ
4cases.2 φ ¬ ψ χ
4cases.3 ¬ φ ψ χ
4cases.4 ¬ φ ¬ ψ χ
Assertion 4cases χ

Proof

Step Hyp Ref Expression
1 4cases.1 φ ψ χ
2 4cases.2 φ ¬ ψ χ
3 4cases.3 ¬ φ ψ χ
4 4cases.4 ¬ φ ¬ ψ χ
5 1 3 pm2.61ian ψ χ
6 2 4 pm2.61ian ¬ ψ χ
7 5 6 pm2.61i χ