Theorem intnanrd 940

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 633	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 619  ax-in2 620

This theorem is referenced by:  dcand  941  bianfd  957  3bior1fand  1390  frecabcl  6608  frecsuclem  6615  xrrebnd  10098  fzpreddisj  10351  iseqf1olemqk  10815  gcdsupex  12591  gcdsupcl  12592  nndvdslegcd  12599  divgcdnn  12609  sqgcd  12663  coprm  12779  pclemdc  12924  1arith  13003  ctiunctlemudc  13121  gsum0g  13542  gsumval2  13543  lgsval2lem  15812  lgsval4a  15824  lgsdilem  15829  trlsegvdegfi  16391