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

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 623  ax-in2 624

This theorem is referenced by:  dcand  945  poxp  6458  cauappcvgprlemladdrl  8014  caucvgprlemladdrl  8035  xrrebnd  10200  fzpreddisj  10456  fzp1nel  10489  fprodntrivap  12329  bitsfzo  12700  bitsmod  12701  gcdsupex  12712  gcdsupcl  12713  gcdnncl  12722  gcd2n0cl  12724  qredeu  12853  cncongr2  12860  divnumden  12952  divdenle  12953  phisum  12997  pythagtriplem4  13025  pythagtriplem8  13029  pythagtriplem9  13030  isnsgrp  13698  ivthinclemdisj  15664  lgsneg  16057  umgredgnlp  16307  umgr2edg1  16364  umgr2edgneu  16367