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:  dcan  934  poxp  6250  cauappcvgprlemladdrl  7673  caucvgprlemladdrl  7694  xrrebnd  9836  fzpreddisj  10088  fzp1nel  10121  fprodntrivap  11609  gcdsupex  11975  gcdsupcl  11976  gcdnncl  11985  gcd2n0cl  11987  qredeu  12114  cncongr2  12121  divnumden  12213  divdenle  12214  phisum  12257  pythagtriplem4  12285  pythagtriplem8  12289  pythagtriplem9  12290  isnsgrp  12834  ivthinclemdisj  14501  lgsneg  14808