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

Theorem intnand 982
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 476 . 2 ((𝜒𝜓) → 𝜓)
31, 2nsyl 135 1 (𝜑 → ¬ (𝜒𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 383
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 197  df-an 385
This theorem is referenced by:  csbxp  5234  poxp  7334  suppss2  7374  supp0cosupp0  7379  imacosupp  7380  cdadom1  9046  cfsuc  9117  axunnd  9456  difreicc  12342  fzpreddisj  12428  fzp1nel  12462  repsundef  13564  cshnz  13584  fprodntriv  14716  bitsfzo  15204  bitsmod  15205  gcdnncl  15276  gcd2n0cl  15278  qredeu  15419  cncongr2  15429  divnumden  15503  divdenle  15504  phisum  15542  pythagtriplem4  15571  pythagtriplem8  15575  pythagtriplem9  15576  isnsgrp  17335  isnmnd  17345  mgm2nsgrplem2  17453  0ringnnzr  19317  frlmssuvc2  20182  mamufacex  20243  mavmulsolcl  20405  maducoeval2  20494  opnfbas  21693  lgsneg  25091  numedglnl  26084  umgredgnlp  26087  umgr2edg1  26148  umgr2edgneu  26151  uhgrnbgr0nb  26295  nfrgr2v  27252  4cycl2vnunb  27270  numclwwlk3lemOLD  27369  divnumden2  29692  poseq  31878  nodenselem8  31966  unbdqndv1  32624  relowlssretop  33341  relowlpssretop  33342  finxpreclem6  33363  itg2addnclem2  33592  elpadd0  35413  dihatlat  36940  dihjatcclem1  37024  rmspecnonsq  37789  rpnnen3lem  37915  gtnelicc  40040  xrgtnelicc  40083  limcrecl  40179  sumnnodd  40180  jumpncnp  40429  stoweidlem39  40574  stoweidlem59  40594  fourierdlem12  40654  preimagelt  41233  preimalegt  41234  pgrpgt2nabl  42472  lindslinindsimp1  42571  lmod1zrnlvec  42608
  Copyright terms: Public domain W3C validator