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  6395  frecsuclem  6402  xrrebnd  9813  fzpreddisj  10064  iseqf1olemqk  10487  gcdsupex  11948  gcdsupcl  11949  nndvdslegcd  11956  divgcdnn  11966  sqgcd  12020  coprm  12134  pclemdc  12278  1arith  12355  ctiunctlemudc  12428  lgsval2lem  14193  lgsval4a  14205  lgsdilem  14210