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  6318  cauappcvgprlemladdrl  7770  caucvgprlemladdrl  7791  xrrebnd  9941  fzpreddisj  10193  fzp1nel  10226  fprodntrivap  11895  bitsfzo  12266  bitsmod  12267  gcdsupex  12278  gcdsupcl  12279  gcdnncl  12288  gcd2n0cl  12290  qredeu  12419  cncongr2  12426  divnumden  12518  divdenle  12519  phisum  12563  pythagtriplem4  12591  pythagtriplem8  12595  pythagtriplem9  12596  isnsgrp  13238  ivthinclemdisj  15112  lgsneg  15501