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:  dcand  934  poxp  6299  cauappcvgprlemladdrl  7741  caucvgprlemladdrl  7762  xrrebnd  9911  fzpreddisj  10163  fzp1nel  10196  fprodntrivap  11766  bitsfzo  12137  bitsmod  12138  gcdsupex  12149  gcdsupcl  12150  gcdnncl  12159  gcd2n0cl  12161  qredeu  12290  cncongr2  12297  divnumden  12389  divdenle  12390  phisum  12434  pythagtriplem4  12462  pythagtriplem8  12466  pythagtriplem9  12467  isnsgrp  13108  ivthinclemdisj  14960  lgsneg  15349