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  6399  frecsuclem  6406  xrrebnd  9817  fzpreddisj  10068  iseqf1olemqk  10491  gcdsupex  11952  gcdsupcl  11953  nndvdslegcd  11960  divgcdnn  11970  sqgcd  12024  coprm  12138  pclemdc  12282  1arith  12359  ctiunctlemudc  12432  lgsval2lem  14304  lgsval4a  14316  lgsdilem  14321