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  1476  pr1eqbg  4881  iresn0n0  6083  fvmptopabOLD  7505  frxp2  8185  frxp3  8192  wemappo  9618  axrepnd  10663  axunnd  10665  fzpreddisj  13633  sadadd2lem2  16496  smumullem  16538  nndvdslegcd  16551  divgcdnn  16561  sqgcd  16609  coprm  16758  isnmnd  18776  nfimdetndef  22616  mdetfval1  22617  ibladdlem  25875  lgsval2lem  27369  lgsval4a  27381  lgsdilem  27386  2sqcoprm  27497  addsqn2reurex2  27507  nosepdmlem  27746  nodenselem8  27754  nosupbnd2lem1  27778  nbgrnself  29394  wwlks  29868  iswspthsnon  29889  clwwlknon1nloop  30131  clwwlknon1le1  30133  nfrgr2v  30304  hashxpe  32814  acycgr0v  35116  prclisacycgr  35119  fmlasucdisj  35367  dfrdg4  35915  finxpreclem3  37359  finxpreclem5  37361  ibladdnclem  37636  dihatlat  41291  xppss12  42222  jm2.23  42953  rexanuz2nf  45408  ltnelicc  45415  limciccioolb  45542  dvmptfprodlem  45865  stoweidlem26  45947  fourierdlem12  46040  fourierdlem42  46070  divgcdoddALTV  47556