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  6402  frecsuclem  6409  xrrebnd  9821  fzpreddisj  10073  iseqf1olemqk  10496  gcdsupex  11960  gcdsupcl  11961  nndvdslegcd  11968  divgcdnn  11978  sqgcd  12032  coprm  12146  pclemdc  12290  1arith  12367  ctiunctlemudc  12440  lgsval2lem  14496  lgsval4a  14508  lgsdilem  14513