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  6468  cauappcvgprlemladdrl  8025  caucvgprlemladdrl  8046  xrrebnd  10232  fzpreddisj  10489  fzp1nel  10522  fprodntrivap  12370  bitsfzo  12741  bitsmod  12742  gcdsupex  12753  gcdsupcl  12754  gcdnncl  12763  gcd2n0cl  12765  qredeu  12894  cncongr2  12901  divnumden  12995  divdenle  12996  phisum  13042  pythagtriplem4  13070  pythagtriplem8  13074  pythagtriplem9  13075  isnsgrp  13774  ivthinclemdisj  15832  lgsneg  16309  umgredgnlp  16559  umgr2edg1  16616  umgr2edgneu  16619