Theorem intnanrd 490

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

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

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 208  df-an 397

This theorem is referenced by:  bianfd  539  3bior1fand  1484  pr1eqbg  4788  iresn0n0  6006  frxp2  8084  frxp3  8091  wemappo  9454  axrepnd  10508  axunnd  10510  fzpreddisj  13518  sadadd2lem2  16410  smumullem  16452  nndvdslegcd  16465  divgcdnn  16475  sqgcd  16522  coprm  16672  isnmnd  18697  nfimdetndef  22572  mdetfval1  22573  ibladdlem  25805  lgsval2lem  27288  lgsval4a  27300  lgsdilem  27305  2sqcoprm  27416  addsqn2reurex2  27426  nosepdmlem  27665  nodenselem8  27673  nosupbnd2lem1  27697  pw2cut2  28472  nbgrnself  29446  wwlks  29921  iswspthsnon  29942  clwwlknon1nloop  30187  clwwlknon1le1  30189  nfrgr2v  30360  tpssad  32627  hashxpe  32899  esplyind  33759  acycgr0v  35376  prclisacycgr  35379  fmlasucdisj  35627  dfrdg4  36179  finxpreclem3  37755  finxpreclem5  37757  ibladdnclem  38043  dihatlat  41826  xppss12  42716  jm2.23  43441  rexanuz2nf  45935  ltnelicc  45942  limciccioolb  46066  dvmptfprodlem  46387  stoweidlem26  46469  fourierdlem12  46562  fourierdlem42  46592  divgcdoddALTV  48173