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  6565  frecsuclem  6572  xrrebnd  10054  fzpreddisj  10306  iseqf1olemqk  10769  gcdsupex  12529  gcdsupcl  12530  nndvdslegcd  12537  divgcdnn  12547  sqgcd  12601  coprm  12717  pclemdc  12862  1arith  12941  ctiunctlemudc  13059  gsum0g  13480  gsumval2  13481  lgsval2lem  15741  lgsval4a  15753  lgsdilem  15758