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 ( 𝜑 → ¬ ( 𝜓𝜒 ) )