Theorem intnand 938

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  940  poxp  6396  cauappcvgprlemladdrl  7876  caucvgprlemladdrl  7897  xrrebnd  10053  fzpreddisj  10305  fzp1nel  10338  fprodntrivap  12144  bitsfzo  12515  bitsmod  12516  gcdsupex  12527  gcdsupcl  12528  gcdnncl  12537  gcd2n0cl  12539  qredeu  12668  cncongr2  12675  divnumden  12767  divdenle  12768  phisum  12812  pythagtriplem4  12840  pythagtriplem8  12844  pythagtriplem9  12845  isnsgrp  13488  ivthinclemdisj  15363  lgsneg  15752  umgredgnlp  16002  umgr2edg1  16059  umgr2edgneu  16062