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  6252  cauappcvgprlemladdrl  7676  caucvgprlemladdrl  7697  xrrebnd  9839  fzpreddisj  10091  fzp1nel  10124  fprodntrivap  11612  gcdsupex  11978  gcdsupcl  11979  gcdnncl  11988  gcd2n0cl  11990  qredeu  12117  cncongr2  12124  divnumden  12216  divdenle  12217  phisum  12260  pythagtriplem4  12288  pythagtriplem8  12292  pythagtriplem9  12293  isnsgrp  12842  ivthinclemdisj  14522  lgsneg  14829