Theorem intnand 491

Description: Introduction of conjunct inside of a contradiction. (Contributed by NM, 10-Jul-2005.)

Hypothesis

Ref	Expression
intnand.1	⊢ (𝜑 → ¬ 𝜓)

Assertion

Ref	Expression
intnand	⊢ (𝜑 → ¬ (𝜒 ∧ 𝜓))

Proof of Theorem intnand

Step	Hyp	Ref	Expression
1		intnand.1	. 2 ⊢ (𝜑 → ¬ 𝜓)
2		simpr 487	. 2 ⊢ ((𝜒 ∧ 𝜓) → 𝜓)
3	1, 2	nsyl 142	1 ⊢ (𝜑 → ¬ (𝜒 ∧ 𝜓))

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

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 209  df-an 399

This theorem is referenced by:  csbxp  5644  poxp  7816  suppss2  7858  suppco  7864  supp0cosupp0OLD  7867  imacosuppOLD  7869  cfsuc  9673  axunnd  10012  difreicc  12864  fzpreddisj  12950  fzp1nel  12985  repsundef  14127  cshnz  14148  fprodntriv  15290  bitsfzo  15778  bitsmod  15779  gcdnncl  15850  gcd2n0cl  15852  qredeu  15996  cncongr2  16006  divnumden  16082  divdenle  16083  phisum  16121  pythagtriplem4  16150  pythagtriplem8  16154  pythagtriplem9  16155  isnsgrp  17899  isnmnd  17909  mgm2nsgrplem2  18078  0ringnnzr  20036  frlmssuvc2  20933  mamufacex  20994  mavmulsolcl  21154  maducoeval2  21243  opnfbas  22444  lgsneg  25891  numedglnl  26923  umgredgnlp  26926  umgr2edg1  26987  umgr2edgneu  26990  uhgrnbgr0nb  27130  nfrgr2v  28045  4cycl2vnunb  28063  hashxpe  30523  divnumden2  30528  fmlasucdisj  32641  poseq  33090  nodenselem8  33190  unbdqndv1  33842  relowlssretop  34638  relowlpssretop  34639  finxpreclem6  34671  itg2addnclem2  34938  elpadd0  36939  dihatlat  38464  dihjatcclem1  38548  rmspecnonsq  39497  rpnnen3lem  39621  gtnelicc  41768  xrgtnelicc  41807  limcrecl  41903  sumnnodd  41904  jumpncnp  42174  stoweidlem39  42318  stoweidlem59  42338  fourierdlem12  42398  preimagelt  42974  preimalegt  42975  pgrpgt2nabl  44408  lindslinindsimp1  44506  lmod1zrnlvec  44543  rrxsphere  44729