Metamath Proof Explorer


Theorem intnanr

Description: Introduction of conjunct inside of a contradiction. (Contributed by NM, 3-Apr-1995)

Ref Expression
Hypothesis intnan.1 ¬ 𝜑
Assertion intnanr ¬ ( 𝜑𝜓 )

Proof

Step Hyp Ref Expression
1 intnan.1 ¬ 𝜑
2 simpl ( ( 𝜑𝜓 ) → 𝜑 )
3 1 2 mto ¬ ( 𝜑𝜓 )