Theorem intnand 931

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 628	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 614  ax-in2 615

This theorem is referenced by:  dcan  933  poxp  6235  cauappcvgprlemladdrl  7658  caucvgprlemladdrl  7679  xrrebnd  9821  fzpreddisj  10073  fzp1nel  10106  fprodntrivap  11594  gcdsupex  11960  gcdsupcl  11961  gcdnncl  11970  gcd2n0cl  11972  qredeu  12099  cncongr2  12106  divnumden  12198  divdenle  12199  phisum  12242  pythagtriplem4  12270  pythagtriplem8  12274  pythagtriplem9  12275  isnsgrp  12817  ivthinclemdisj  14157  lgsneg  14464