Theorem intnand 939

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 110	. 2 ⊢ ((𝜒 ∧ 𝜓) → 𝜓)
3	1, 2	nsyl 633	1 ⊢ (𝜑 → ¬ (𝜒 ∧ 𝜓))

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 107  ax-in1 619  ax-in2 620

This theorem is referenced by:  dcand  941  poxp  6406  cauappcvgprlemladdrl  7920  caucvgprlemladdrl  7941  xrrebnd  10098  fzpreddisj  10351  fzp1nel  10384  fprodntrivap  12208  bitsfzo  12579  bitsmod  12580  gcdsupex  12591  gcdsupcl  12592  gcdnncl  12601  gcd2n0cl  12603  qredeu  12732  cncongr2  12739  divnumden  12831  divdenle  12832  phisum  12876  pythagtriplem4  12904  pythagtriplem8  12908  pythagtriplem9  12909  isnsgrp  13552  ivthinclemdisj  15434  lgsneg  15826  umgredgnlp  16076  umgr2edg1  16133  umgr2edgneu  16136