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

Theorem intnand 961
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 477 . 2 ((𝜒𝜓) → 𝜓)
31, 2nsyl 135 1 (𝜑 → ¬ (𝜒𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 384
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 386
This theorem is referenced by:  csbxp  5166  poxp  7235  suppss2  7275  supp0cosupp0  7280  imacosupp  7281  cdadom1  8953  cfsuc  9024  axunnd  9363  difreicc  12243  fzpreddisj  12329  fzp1nel  12362  repsundef  13450  cshnz  13470  fprodntriv  14592  bitsfzo  15076  bitsmod  15077  gcdnncl  15148  gcd2n0cl  15150  qredeu  15291  cncongr2  15301  divnumden  15375  divdenle  15376  phisum  15414  pythagtriplem4  15443  pythagtriplem8  15447  pythagtriplem9  15448  isnsgrp  17204  isnmnd  17214  mgm2nsgrplem2  17322  0ringnnzr  19183  frlmssuvc2  20048  mamufacex  20109  mavmulsolcl  20271  maducoeval2  20360  opnfbas  21551  lgsneg  24941  umgredgnlp  25930  umgr2edg1  25990  umgr2edgneu  25993  uhgrnbgr0nb  26131  nfrgr2v  26994  4cycl2vnunb  27012  numclwwlkffin0  27065  numclwwlk3lem  27090  divnumden2  29397  poseq  31443  nodenselem8  31543  unbdqndv1  32133  relowlssretop  32835  relowlpssretop  32836  finxpreclem6  32857  itg2addnclem2  33080  elpadd0  34561  dihatlat  36089  dihjatcclem1  36173  rmspecnonsq  36938  rpnnen3lem  37064  gtnelicc  39120  xrgtnelicc  39163  limcrecl  39252  sumnnodd  39253  jumpncnp  39402  stoweidlem39  39550  stoweidlem59  39570  fourierdlem12  39630  preimagelt  40206  preimalegt  40207  pgrpgt2nabl  41409  lindslinindsimp1  41508  lmod1zrnlvec  41545
  Copyright terms: Public domain W3C validator