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  1479  pr1eqbg  4801  iresn0n0  6011  frxp2  8085  frxp3  8092  wemappo  9455  axrepnd  10506  axunnd  10508  fzpreddisj  13490  sadadd2lem2  16378  smumullem  16420  nndvdslegcd  16433  divgcdnn  16443  sqgcd  16490  coprm  16639  isnmnd  18664  nfimdetndef  22532  mdetfval1  22533  ibladdlem  25765  lgsval2lem  27258  lgsval4a  27270  lgsdilem  27275  2sqcoprm  27386  addsqn2reurex2  27396  nosepdmlem  27635  nodenselem8  27643  nosupbnd2lem1  27667  pw2cut2  28442  nbgrnself  29416  wwlks  29892  iswspthsnon  29913  clwwlknon1nloop  30158  clwwlknon1le1  30160  nfrgr2v  30331  tpssad  32598  hashxpe  32870  esplyind  33724  acycgr0v  35336  prclisacycgr  35339  fmlasucdisj  35587  dfrdg4  36139  finxpreclem3  37705  finxpreclem5  37707  ibladdnclem  37988  dihatlat  41771  xppss12  42662  jm2.23  43427  rexanuz2nf  45924  ltnelicc  45931  limciccioolb  46055  dvmptfprodlem  46376  stoweidlem26  46458  fourierdlem12  46551  fourierdlem42  46581  divgcdoddALTV  48116