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  6551  frecsuclem  6558  xrrebnd  10027  fzpreddisj  10279  iseqf1olemqk  10741  gcdsupex  12493  gcdsupcl  12494  nndvdslegcd  12501  divgcdnn  12511  sqgcd  12565  coprm  12681  pclemdc  12826  1arith  12905  ctiunctlemudc  13023  gsum0g  13444  gsumval2  13445  lgsval2lem  15704  lgsval4a  15716  lgsdilem  15721