Theorem intnand 917

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 109	. 2 ⊢ ((𝜒 ∧ 𝜓) → 𝜓)
3	1, 2	nsyl 618	1 ⊢ (𝜑 → ¬ (𝜒 ∧ 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 106  ax-in1 604  ax-in2 605

This theorem is referenced by:  dcan  919  poxp  6176  cauappcvgprlemladdrl  7571  caucvgprlemladdrl  7592  xrrebnd  9716  fzpreddisj  9966  fzp1nel  9999  fprodntrivap  11474  gcdsupex  11832  gcdsupcl  11833  gcdnncl  11842  gcd2n0cl  11844  qredeu  11965  cncongr2  11972  divnumden  12061  divdenle  12062  phisum  12103  ivthinclemdisj  12989