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  6137  cauappcvgprlemladdrl  7489  caucvgprlemladdrl  7510  xrrebnd  9632  fzpreddisj  9882  fzp1nel  9915  gcdsupex  11682  gcdsupcl  11683  gcdnncl  11692  gcd2n0cl  11694  qredeu  11814  cncongr2  11821  divnumden  11910  divdenle  11911  ivthinclemdisj  12826