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  4810  iresn0n0  6010  frxp2  8083  frxp3  8090  wemappo  9446  axrepnd  10496  axunnd  10498  fzpreddisj  13480  sadadd2lem2  16368  smumullem  16410  nndvdslegcd  16423  divgcdnn  16433  sqgcd  16480  coprm  16629  isnmnd  18654  nfimdetndef  22524  mdetfval1  22525  ibladdlem  25768  lgsval2lem  27265  lgsval4a  27277  lgsdilem  27282  2sqcoprm  27393  addsqn2reurex2  27403  nosepdmlem  27642  nodenselem8  27650  nosupbnd2lem1  27674  pw2cut2  28402  nbgrnself  29358  wwlks  29834  iswspthsnon  29855  clwwlknon1nloop  30100  clwwlknon1le1  30102  nfrgr2v  30273  tpssad  32540  hashxpe  32815  esplyind  33659  acycgr0v  35264  prclisacycgr  35267  fmlasucdisj  35515  dfrdg4  36067  finxpreclem3  37510  finxpreclem5  37512  ibladdnclem  37789  dihatlat  41506  xppss12  42400  jm2.23  43153  rexanuz2nf  45652  ltnelicc  45659  limciccioolb  45783  dvmptfprodlem  46104  stoweidlem26  46186  fourierdlem12  46279  fourierdlem42  46309  divgcdoddALTV  47844