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  6560  frecsuclem  6567  xrrebnd  10044  fzpreddisj  10296  iseqf1olemqk  10759  gcdsupex  12518  gcdsupcl  12519  nndvdslegcd  12526  divgcdnn  12536  sqgcd  12590  coprm  12706  pclemdc  12851  1arith  12930  ctiunctlemudc  13048  gsum0g  13469  gsumval2  13470  lgsval2lem  15729  lgsval4a  15741  lgsdilem  15746