Theorem intnand 490

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

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

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 206  df-an 398

This theorem is referenced by:  csbxp  5697  poxp  8000  suppss2  8047  suppco  8053  cfsuc  10059  axunnd  10398  difreicc  13262  fzpreddisj  13351  fzp1nel  13386  repsundef  14529  cshnz  14550  fprodntriv  15697  bitsfzo  16187  bitsmod  16188  gcdnncl  16259  gcd2n0cl  16261  qredeu  16408  cncongr2  16418  divnumden  16497  divdenle  16498  phisum  16536  pythagtriplem4  16565  pythagtriplem8  16569  pythagtriplem9  16570  cat1lem  17856  isnsgrp  18424  isnmnd  18434  mgm2nsgrplem2  18603  0ringnnzr  20585  frlmssuvc2  21047  mamufacex  21583  mavmulsolcl  21745  maducoeval2  21834  opnfbas  23038  lgsneg  26514  numedglnl  27559  umgredgnlp  27562  umgr2edg1  27623  umgr2edgneu  27626  uhgrnbgr0nb  27766  nfrgr2v  28681  4cycl2vnunb  28699  hashxpe  31172  divnumden2  31177  fmlasucdisj  33406  frxp3  33842  poseq  33847  nodenselem8  33939  noinfbnd2lem1  33978  unbdqndv1  34733  relowlssretop  35578  relowlpssretop  35579  finxpreclem6  35611  itg2addnclem2  35873  elpadd0  37865  dihatlat  39390  dihjatcclem1  39474  aks4d1p8d1  40134  sticksstones22  40166  rmspecnonsq  40766  rpnnen3lem  40891  gtnelicc  43087  xrgtnelicc  43125  limcrecl  43219  sumnnodd  43220  jumpncnp  43488  stoweidlem39  43629  stoweidlem59  43649  fourierdlem12  43709  preimagelt  44287  preimalegt  44288  pgrpgt2nabl  45760  lindslinindsimp1  45856  lmod1zrnlvec  45893  rrxsphere  46152