Theorem intnanrd 944

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 637	1 ⊢ (𝜑 → ¬ (𝜓 ∧ 𝜒))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-in1 623  ax-in2 624

This theorem is used by:  dcand  945  bianfd  961  3bior1fand  1394  frecabcl  6670  frecsuclem  6677  xrrebnd  10231  fzpreddisj  10488  iseqf1olemqk  10957  gcdsupex  12750  gcdsupcl  12751  nndvdslegcd  12758  divgcdnn  12768  sqgcd  12822  coprm  12939  pclemdc  13087  1arith  13166  ctiunctlemudc  13377  gzsum0  13762  gzsumval2  13763  lgsval2lem  16227  lgsval4a  16239  lgsdilem  16244  trlsegvdegfi  16806