Theorem intnand 484

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

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

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 199  df-an 387

This theorem is referenced by:  csbxp  5448  poxp  7570  suppss2  7611  supp0cosupp0  7616  imacosupp  7617  cdadom1  9343  cfsuc  9414  axunnd  9753  difreicc  12621  fzpreddisj  12707  fzp1nel  12742  repsundef  13917  cshnz  13941  cshnzOLD  13942  fprodntriv  15075  bitsfzo  15563  bitsmod  15564  gcdnncl  15635  gcd2n0cl  15637  qredeu  15777  cncongr2  15787  divnumden  15860  divdenle  15861  phisum  15899  pythagtriplem4  15928  pythagtriplem8  15932  pythagtriplem9  15933  isnsgrp  17674  isnmnd  17684  mgm2nsgrplem2  17793  0ringnnzr  19666  frlmssuvc2  20538  mamufacex  20599  mavmulsolcl  20762  maducoeval2  20851  opnfbas  22054  lgsneg  25498  numedglnl  26493  umgredgnlp  26496  umgr2edg1  26557  umgr2edgneu  26560  uhgrnbgr0nb  26701  nfrgr2v  27680  4cycl2vnunb  27698  divnumden2  30128  poseq  32342  nodenselem8  32430  unbdqndv1  33081  relowlssretop  33806  relowlpssretop  33807  finxpreclem6  33828  itg2addnclem2  34087  elpadd0  35963  dihatlat  37488  dihjatcclem1  37572  rmspecnonsq  38431  rpnnen3lem  38557  gtnelicc  40634  xrgtnelicc  40673  limcrecl  40769  sumnnodd  40770  jumpncnp  41039  stoweidlem39  41183  stoweidlem59  41203  fourierdlem12  41263  preimagelt  41839  preimalegt  41840  pgrpgt2nabl  43162  lindslinindsimp1  43261  lmod1zrnlvec  43298  rrxsphere  43484