Theorem intnand 936

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 631	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 617  ax-in2 618

This theorem is referenced by:  dcand  938  poxp  6392  cauappcvgprlemladdrl  7867  caucvgprlemladdrl  7888  xrrebnd  10044  fzpreddisj  10296  fzp1nel  10329  fprodntrivap  12135  bitsfzo  12506  bitsmod  12507  gcdsupex  12518  gcdsupcl  12519  gcdnncl  12528  gcd2n0cl  12530  qredeu  12659  cncongr2  12666  divnumden  12758  divdenle  12759  phisum  12803  pythagtriplem4  12831  pythagtriplem8  12835  pythagtriplem9  12836  isnsgrp  13479  ivthinclemdisj  15354  lgsneg  15743  umgredgnlp  15991  umgr2edg1  16048  umgr2edgneu  16051