Theorem intnand 932

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 629	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 615  ax-in2 616

This theorem is referenced by:  dcan  934  poxp  6246  cauappcvgprlemladdrl  7669  caucvgprlemladdrl  7690  xrrebnd  9832  fzpreddisj  10084  fzp1nel  10117  fprodntrivap  11605  gcdsupex  11971  gcdsupcl  11972  gcdnncl  11981  gcd2n0cl  11983  qredeu  12110  cncongr2  12117  divnumden  12209  divdenle  12210  phisum  12253  pythagtriplem4  12281  pythagtriplem8  12285  pythagtriplem9  12286  isnsgrp  12830  ivthinclemdisj  14389  lgsneg  14696