Theorem intnand 921

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

Hypothesis

Ref	Expression
intnand.1	⊢ (𝜑 → ¬ 𝜓)

Assertion

Ref	Expression
intnand	⊢ (𝜑 → ¬ (𝜒 ∧ 𝜓))

Proof of Theorem intnand

Step	Hyp	Ref	Expression
1		intnand.1	. 2 ⊢ (𝜑 → ¬ 𝜓)
2		simpr 109	. 2 ⊢ ((𝜒 ∧ 𝜓) → 𝜓)
3	1, 2	nsyl 618	1 ⊢ (𝜑 → ¬ (𝜒 ∧ 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 106  ax-in1 604  ax-in2 605

This theorem is referenced by:  dcan  923  poxp  6196  cauappcvgprlemladdrl  7594  caucvgprlemladdrl  7615  xrrebnd  9751  fzpreddisj  10002  fzp1nel  10035  fprodntrivap  11521  gcdsupex  11886  gcdsupcl  11887  gcdnncl  11896  gcd2n0cl  11898  qredeu  12025  cncongr2  12032  divnumden  12124  divdenle  12125  phisum  12168  pythagtriplem4  12196  pythagtriplem8  12200  pythagtriplem9  12201  ivthinclemdisj  13218  lgsneg  13525