Theorem intnand 873

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 108	. 2 ⊢ ((𝜒 ∧ 𝜓) → 𝜓)
3	1, 2	nsyl 590	1 ⊢ (𝜑 → ¬ (𝜒 ∧ 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 102

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia2 105  ax-in1 576  ax-in2 577

This theorem is referenced by:  dcan  875  poxp  5873  cauappcvgprlemladdrl  6847  caucvgprlemladdrl  6868  xrrebnd  8886  fzpreddisj  9088  fzp1nel  9121  gcdsupex  10349  gcdsupcl  10350  gcdnncl  10359  gcd2n0cl  10361  qredeu  10479  cncongr2  10486