Theorem intnanrd 934

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  935  bianfd  951  3bior1fand  1365  frecabcl  6498  frecsuclem  6505  xrrebnd  9961  fzpreddisj  10213  iseqf1olemqk  10674  gcdsupex  12353  gcdsupcl  12354  nndvdslegcd  12361  divgcdnn  12371  sqgcd  12425  coprm  12541  pclemdc  12686  1arith  12765  ctiunctlemudc  12883  gsum0g  13303  gsumval2  13304  lgsval2lem  15562  lgsval4a  15574  lgsdilem  15579