MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  intnand Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 intnand.1 . 2 (𝜑 → ¬ 𝜓)
2 simpr 479 . 2 ((𝜒𝜓) → 𝜓)
31, 2nsyl 138 1 (𝜑 → ¬ (𝜒𝜓))
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator