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  3bior1fand  1364  frecabcl  6475  frecsuclem  6482  xrrebnd  9923  fzpreddisj  10175  iseqf1olemqk  10633  gcdsupex  12197  gcdsupcl  12198  nndvdslegcd  12205  divgcdnn  12215  sqgcd  12269  coprm  12385  pclemdc  12530  1arith  12609  ctiunctlemudc  12727  gsum0g  13146  gsumval2  13147  lgsval2lem  15405  lgsval4a  15417  lgsdilem  15422