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  6013  frxp2  8087  frxp3  8094  wemappo  9457  axrepnd  10508  axunnd  10510  fzpreddisj  13518  sadadd2lem2  16410  smumullem  16452  nndvdslegcd  16465  divgcdnn  16475  sqgcd  16522  coprm  16672  isnmnd  18697  nfimdetndef  22564  mdetfval1  22565  ibladdlem  25797  lgsval2lem  27284  lgsval4a  27296  lgsdilem  27301  2sqcoprm  27412  addsqn2reurex2  27422  nosepdmlem  27661  nodenselem8  27669  nosupbnd2lem1  27693  pw2cut2  28468  nbgrnself  29442  wwlks  29918  iswspthsnon  29939  clwwlknon1nloop  30184  clwwlknon1le1  30186  nfrgr2v  30357  tpssad  32624  hashxpe  32895  esplyind  33734  acycgr0v  35346  prclisacycgr  35349  fmlasucdisj  35597  dfrdg4  36149  finxpreclem3  37723  finxpreclem5  37725  ibladdnclem  38011  dihatlat  41794  xppss12  42684  jm2.23  43442  rexanuz2nf  45938  ltnelicc  45945  limciccioolb  46069  dvmptfprodlem  46390  stoweidlem26  46472  fourierdlem12  46565  fourierdlem42  46595  divgcdoddALTV  48170