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  6299  cauappcvgprlemladdrl  7743  caucvgprlemladdrl  7764  xrrebnd  9913  fzpreddisj  10165  fzp1nel  10198  fprodntrivap  11768  bitsfzo  12139  bitsmod  12140  gcdsupex  12151  gcdsupcl  12152  gcdnncl  12161  gcd2n0cl  12163  qredeu  12292  cncongr2  12299  divnumden  12391  divdenle  12392  phisum  12436  pythagtriplem4  12464  pythagtriplem8  12468  pythagtriplem9  12469  isnsgrp  13110  ivthinclemdisj  14962  lgsneg  15351