Theorem intnanrd 932

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 628	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 614  ax-in2 615

This theorem is referenced by:  dcan  933  bianfd  948  frecabcl  6400  frecsuclem  6407  xrrebnd  9819  fzpreddisj  10071  iseqf1olemqk  10494  gcdsupex  11958  gcdsupcl  11959  nndvdslegcd  11966  divgcdnn  11976  sqgcd  12030  coprm  12144  pclemdc  12288  1arith  12365  ctiunctlemudc  12438  lgsval2lem  14414  lgsval4a  14426  lgsdilem  14431