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  10237  fzpreddisj  10494  fzp1nel  10527  fprodntrivap  12375  bitsfzo  12746  bitsmod  12747  gcdsupex  12758  gcdsupcl  12759  gcdnncl  12768  gcd2n0cl  12770  qredeu  12899  cncongr2  12906  divnumden  13000  divdenle  13001  phisum  13047  pythagtriplem4  13075  pythagtriplem8  13079  pythagtriplem9  13080  isnsgrp  13779  ivthinclemdisj  15883  lgsneg  16365  umgredgnlp  16615  umgr2edg1  16672  umgr2edgneu  16675