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  8024  caucvgprlemladdrl  8045  xrrebnd  10231  fzpreddisj  10488  fzp1nel  10521  fprodntrivap  12367  bitsfzo  12738  bitsmod  12739  gcdsupex  12750  gcdsupcl  12751  gcdnncl  12760  gcd2n0cl  12762  qredeu  12891  cncongr2  12898  divnumden  12992  divdenle  12993  phisum  13039  pythagtriplem4  13067  pythagtriplem8  13071  pythagtriplem9  13072  isnsgrp  13770  ivthinclemdisj  15790  lgsneg  16241  umgredgnlp  16491  umgr2edg1  16548  umgr2edgneu  16551