Metamath Proof Explorer


Theorem pm2.21dd

Description: A contradiction implies anything. Deduction from pm2.21 . (Contributed by Mario Carneiro, 9-Feb-2017) (Proof shortened by Wolf Lammen, 22-Jul-2019)

Ref Expression
Hypotheses pm2.21dd.1 φ ψ
pm2.21dd.2 φ ¬ ψ
Assertion pm2.21dd φ χ

Proof

Step Hyp Ref Expression
1 pm2.21dd.1 φ ψ
2 pm2.21dd.2 φ ¬ ψ
3 1 2 pm2.65i ¬ φ
4 3 pm2.21i φ χ