Theorem intnand 916

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 617	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 603  ax-in2 604

This theorem is referenced by:  dcan  918  poxp  6122  cauappcvgprlemladdrl  7458  caucvgprlemladdrl  7479  xrrebnd  9595  fzpreddisj  9844  fzp1nel  9877  gcdsupex  11635  gcdsupcl  11636  gcdnncl  11645  gcd2n0cl  11647  qredeu  11767  cncongr2  11774  divnumden  11863  divdenle  11864  ivthinclemdisj  12776