Theorem intnand 943

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 637	1 ⊢ (𝜑 → ¬ (𝜒 ∧ 𝜓))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 107  ax-in1 623  ax-in2 624

This theorem is used by:  dcand  945  poxp  6472  cauappcvgprlemladdrl  8030  caucvgprlemladdrl  8051  xrrebnd  10238  fzpreddisj  10495  fzp1nel  10528  fprodntrivap  12376  bitsfzo  12747  bitsmod  12748  gcdsupex  12759  gcdsupcl  12760  gcdnncl  12769  gcd2n0cl  12771  qredeu  12900  cncongr2  12907  divnumden  13001  divdenle  13002  phisum  13048  pythagtriplem4  13076  pythagtriplem8  13080  pythagtriplem9  13081  isnsgrp  13780  ivthinclemdisj  15866  lgsneg  16348  umgredgnlp  16598  umgr2edg1  16655  umgr2edgneu  16658