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  10770  gcdsupex  12533  gcdsupcl  12534  nndvdslegcd  12541  divgcdnn  12551  sqgcd  12605  coprm  12721  pclemdc  12866  1arith  12945  ctiunctlemudc  13063  gsum0g  13484  gsumval2  13485  lgsval2lem  15745  lgsval4a  15757  lgsdilem  15762  trlsegvdegfi  16324