Theorem intnand 936

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 631	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 617  ax-in2 618

This theorem is referenced by:  dcand  938  poxp  6384  cauappcvgprlemladdrl  7855  caucvgprlemladdrl  7876  xrrebnd  10027  fzpreddisj  10279  fzp1nel  10312  fprodntrivap  12110  bitsfzo  12481  bitsmod  12482  gcdsupex  12493  gcdsupcl  12494  gcdnncl  12503  gcd2n0cl  12505  qredeu  12634  cncongr2  12641  divnumden  12733  divdenle  12734  phisum  12778  pythagtriplem4  12806  pythagtriplem8  12810  pythagtriplem9  12811  isnsgrp  13454  ivthinclemdisj  15329  lgsneg  15718  umgredgnlp  15965  umgr2edg1  16022  umgr2edgneu  16025