Metamath Proof Explorer


Theorem intnanrd

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

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

Proof

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