Theorem intnand 933

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  935  poxp  6341  cauappcvgprlemladdrl  7805  caucvgprlemladdrl  7826  xrrebnd  9976  fzpreddisj  10228  fzp1nel  10261  fprodntrivap  12010  bitsfzo  12381  bitsmod  12382  gcdsupex  12393  gcdsupcl  12394  gcdnncl  12403  gcd2n0cl  12405  qredeu  12534  cncongr2  12541  divnumden  12633  divdenle  12634  phisum  12678  pythagtriplem4  12706  pythagtriplem8  12710  pythagtriplem9  12711  isnsgrp  13353  ivthinclemdisj  15227  lgsneg  15616  umgredgnlp  15856