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  6643  frecsuclem  6650  xrrebnd  10171  fzpreddisj  10427  iseqf1olemqk  10893  gcdsupex  12678  gcdsupcl  12679  nndvdslegcd  12686  divgcdnn  12696  sqgcd  12750  coprm  12866  pclemdc  13011  1arith  13090  ctiunctlemudc  13272  gsum0g  13659  gsumval2  13660  lgsval2lem  16009  lgsval4a  16021  lgsdilem  16026  trlsegvdegfi  16588