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

Theorem intnand 1000
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 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  5357  poxp  7457  suppss2  7498  supp0cosupp0  7503  imacosupp  7504  cdadom1  9200  cfsuc  9271  axunnd  9610  difreicc  12497  fzpreddisj  12583  fzp1nel  12617  repsundef  13718  cshnz  13738  fprodntriv  14871  bitsfzo  15359  bitsmod  15360  gcdnncl  15431  gcd2n0cl  15433  qredeu  15574  cncongr2  15584  divnumden  15658  divdenle  15659  phisum  15697  pythagtriplem4  15726  pythagtriplem8  15730  pythagtriplem9  15731  isnsgrp  17489  isnmnd  17499  mgm2nsgrplem2  17607  0ringnnzr  19471  frlmssuvc2  20336  mamufacex  20397  mavmulsolcl  20559  maducoeval2  20648  opnfbas  21847  lgsneg  25245  numedglnl  26238  umgredgnlp  26241  umgr2edg1  26302  umgr2edgneu  26305  uhgrnbgr0nb  26449  nfrgr2v  27426  4cycl2vnunb  27444  numclwwlk3lemOLD  27550  divnumden2  29873  poseq  32059  nodenselem8  32147  unbdqndv1  32805  relowlssretop  33522  relowlpssretop  33523  finxpreclem6  33544  itg2addnclem2  33775  elpadd0  35598  dihatlat  37125  dihjatcclem1  37209  rmspecnonsq  37974  rpnnen3lem  38100  gtnelicc  40225  xrgtnelicc  40268  limcrecl  40364  sumnnodd  40365  jumpncnp  40614  stoweidlem39  40759  stoweidlem59  40779  fourierdlem12  40839  preimagelt  41418  preimalegt  41419  pgrpgt2nabl  42657  lindslinindsimp1  42756  lmod1zrnlvec  42793
  Copyright terms: Public domain W3C validator