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  6441  cauappcvgprlemladdrl  7988  caucvgprlemladdrl  8009  xrrebnd  10171  fzpreddisj  10427  fzp1nel  10460  fprodntrivap  12295  bitsfzo  12666  bitsmod  12667  gcdsupex  12678  gcdsupcl  12679  gcdnncl  12688  gcd2n0cl  12690  qredeu  12819  cncongr2  12826  divnumden  12918  divdenle  12919  phisum  12963  pythagtriplem4  12991  pythagtriplem8  12995  pythagtriplem9  12996  isnsgrp  13669  ivthinclemdisj  15631  lgsneg  16023  umgredgnlp  16273  umgr2edg1  16330  umgr2edgneu  16333