Metamath Proof Explorer


Theorem intnand

Description: Introduction of conjunct inside of a contradiction. (Contributed by NM, 10-Jul-2005)

Ref Expression
Hypothesis intnand.1 φ ¬ ψ
Assertion intnand φ ¬ χ ψ

Proof

Step Hyp Ref Expression
1 intnand.1 φ ¬ ψ
2 simpr χ ψ ψ
3 1 2 nsyl φ ¬ χ ψ