Theorem intnanrd 939

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  940  bianfd  956  3bior1fand  1389  frecabcl  6564  frecsuclem  6571  xrrebnd  10053  fzpreddisj  10305  iseqf1olemqk  10768  gcdsupex  12527  gcdsupcl  12528  nndvdslegcd  12535  divgcdnn  12545  sqgcd  12599  coprm  12715  pclemdc  12860  1arith  12939  ctiunctlemudc  13057  gsum0g  13478  gsumval2  13479  lgsval2lem  15738  lgsval4a  15750  lgsdilem  15755