Theorem intnanrd 489

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 482	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜓)
3	1, 2	nsyl 140	1 ⊢ (𝜑 → ¬ (𝜓 ∧ 𝜒))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396

This theorem is referenced by:  bianfd  534  3bior1fand  1478  pr1eqbg  4813  iresn0n0  6013  frxp2  8086  frxp3  8093  wemappo  9454  axrepnd  10505  axunnd  10507  fzpreddisj  13489  sadadd2lem2  16377  smumullem  16419  nndvdslegcd  16432  divgcdnn  16442  sqgcd  16489  coprm  16638  isnmnd  18663  nfimdetndef  22533  mdetfval1  22534  ibladdlem  25777  lgsval2lem  27274  lgsval4a  27286  lgsdilem  27291  2sqcoprm  27402  addsqn2reurex2  27412  nosepdmlem  27651  nodenselem8  27659  nosupbnd2lem1  27683  pw2cut2  28458  nbgrnself  29432  wwlks  29908  iswspthsnon  29929  clwwlknon1nloop  30174  clwwlknon1le1  30176  nfrgr2v  30347  tpssad  32614  hashxpe  32887  esplyind  33731  acycgr0v  35342  prclisacycgr  35345  fmlasucdisj  35593  dfrdg4  36145  finxpreclem3  37598  finxpreclem5  37600  ibladdnclem  37877  dihatlat  41594  xppss12  42485  jm2.23  43238  rexanuz2nf  45736  ltnelicc  45743  limciccioolb  45867  dvmptfprodlem  46188  stoweidlem26  46270  fourierdlem12  46363  fourierdlem42  46393  divgcdoddALTV  47928