Theorem intnanrd 937

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 631	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 617  ax-in2 618

This theorem is referenced by:  dcand  938  bianfd  954  3bior1fand  1387  frecabcl  6543  frecsuclem  6550  xrrebnd  10011  fzpreddisj  10263  iseqf1olemqk  10724  gcdsupex  12473  gcdsupcl  12474  nndvdslegcd  12481  divgcdnn  12491  sqgcd  12545  coprm  12661  pclemdc  12806  1arith  12885  ctiunctlemudc  13003  gsum0g  13424  gsumval2  13425  lgsval2lem  15683  lgsval4a  15695  lgsdilem  15700