Theorem intnand 931

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 628	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 614  ax-in2 615

This theorem is referenced by:  dcan  933  poxp  6228  cauappcvgprlemladdrl  7651  caucvgprlemladdrl  7672  xrrebnd  9813  fzpreddisj  10064  fzp1nel  10097  fprodntrivap  11583  gcdsupex  11948  gcdsupcl  11949  gcdnncl  11958  gcd2n0cl  11960  qredeu  12087  cncongr2  12094  divnumden  12186  divdenle  12187  phisum  12230  pythagtriplem4  12258  pythagtriplem8  12262  pythagtriplem9  12263  isnsgrp  12742  ivthinclemdisj  13900  lgsneg  14207