Theorem intnand 936

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 631	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 617  ax-in2 618

This theorem is referenced by:  dcand  938  poxp  6376  cauappcvgprlemladdrl  7840  caucvgprlemladdrl  7861  xrrebnd  10011  fzpreddisj  10263  fzp1nel  10296  fprodntrivap  12090  bitsfzo  12461  bitsmod  12462  gcdsupex  12473  gcdsupcl  12474  gcdnncl  12483  gcd2n0cl  12485  qredeu  12614  cncongr2  12621  divnumden  12713  divdenle  12714  phisum  12758  pythagtriplem4  12786  pythagtriplem8  12790  pythagtriplem9  12791  isnsgrp  13434  ivthinclemdisj  15308  lgsneg  15697  umgredgnlp  15944  umgr2edg1  16001  umgr2edgneu  16004