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  6428  cauappcvgprlemladdrl  7972  caucvgprlemladdrl  7993  xrrebnd  10152  fzpreddisj  10405  fzp1nel  10438  fprodntrivap  12270  bitsfzo  12641  bitsmod  12642  gcdsupex  12653  gcdsupcl  12654  gcdnncl  12663  gcd2n0cl  12665  qredeu  12794  cncongr2  12801  divnumden  12893  divdenle  12894  phisum  12938  pythagtriplem4  12966  pythagtriplem8  12970  pythagtriplem9  12971  isnsgrp  13619  ivthinclemdisj  15505  lgsneg  15897  umgredgnlp  16147  umgr2edg1  16204  umgr2edgneu  16207