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  4838  iresn0n0  6046  fvmptopabOLD  7467  frxp2  8148  frxp3  8155  wemappo  9568  axrepnd  10613  axunnd  10615  fzpreddisj  13595  sadadd2lem2  16474  smumullem  16516  nndvdslegcd  16529  divgcdnn  16539  sqgcd  16586  coprm  16735  isnmnd  18721  nfimdetndef  22532  mdetfval1  22533  ibladdlem  25778  lgsval2lem  27275  lgsval4a  27287  lgsdilem  27292  2sqcoprm  27403  addsqn2reurex2  27413  nosepdmlem  27652  nodenselem8  27660  nosupbnd2lem1  27684  nbgrnself  29343  wwlks  29822  iswspthsnon  29843  clwwlknon1nloop  30085  clwwlknon1le1  30087  nfrgr2v  30258  tpssad  32525  hashxpe  32791  acycgr0v  35175  prclisacycgr  35178  fmlasucdisj  35426  dfrdg4  35974  finxpreclem3  37416  finxpreclem5  37418  ibladdnclem  37705  dihatlat  41358  xppss12  42247  jm2.23  42995  rexanuz2nf  45499  ltnelicc  45506  limciccioolb  45630  dvmptfprodlem  45953  stoweidlem26  46035  fourierdlem12  46128  fourierdlem42  46158  divgcdoddALTV  47676