Theorem intnanrd 933

Description: Introduction of conjunct inside of a contradiction. (Contributed by NM, 10-Jul-2005.)

Hypothesis

Ref	Expression
intnand.1	⊢ (𝜑 → ¬ 𝜓)

Assertion

Ref	Expression
intnanrd	⊢ (𝜑 → ¬ (𝜓 ∧ 𝜒))

Proof of Theorem intnanrd

Step	Hyp	Ref	Expression
1		intnand.1	. 2 ⊢ (𝜑 → ¬ 𝜓)
2		simpl 109	. 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-ia1 106  ax-in1 615  ax-in2 616

This theorem is referenced by:  dcand  934  bianfd  950  frecabcl  6466  frecsuclem  6473  xrrebnd  9913  fzpreddisj  10165  iseqf1olemqk  10618  gcdsupex  12151  gcdsupcl  12152  nndvdslegcd  12159  divgcdnn  12169  sqgcd  12223  coprm  12339  pclemdc  12484  1arith  12563  ctiunctlemudc  12681  gsum0g  13100  gsumval2  13101  lgsval2lem  15359  lgsval4a  15371  lgsdilem  15376