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  6272  cauappcvgprlemladdrl  7703  caucvgprlemladdrl  7724  xrrebnd  9871  fzpreddisj  10123  fzp1nel  10156  fprodntrivap  11701  gcdsupex  12068  gcdsupcl  12069  gcdnncl  12078  gcd2n0cl  12080  qredeu  12209  cncongr2  12216  divnumden  12308  divdenle  12309  phisum  12352  pythagtriplem4  12380  pythagtriplem8  12384  pythagtriplem9  12385  isnsgrp  12963  ivthinclemdisj  14751  lgsneg  15068