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  6336  cauappcvgprlemladdrl  7800  caucvgprlemladdrl  7821  xrrebnd  9971  fzpreddisj  10223  fzp1nel  10256  fprodntrivap  11980  bitsfzo  12351  bitsmod  12352  gcdsupex  12363  gcdsupcl  12364  gcdnncl  12373  gcd2n0cl  12375  qredeu  12504  cncongr2  12511  divnumden  12603  divdenle  12604  phisum  12648  pythagtriplem4  12676  pythagtriplem8  12680  pythagtriplem9  12681  isnsgrp  13323  ivthinclemdisj  15197  lgsneg  15586  umgredgnlp  15826