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

Theorem intnand 492
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 488 . 2 ((𝜒𝜓) → 𝜓)
31, 2nsyl 142 1 (𝜑 → ¬ (𝜒𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 399
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 210  df-an 400
This theorem is referenced by:  csbxp  5623  poxp  7797  suppss2  7839  suppco  7845  supp0cosupp0OLD  7848  imacosuppOLD  7850  cfsuc  9656  axunnd  9995  difreicc  12852  fzpreddisj  12939  fzp1nel  12974  repsundef  14112  cshnz  14133  fprodntriv  15275  bitsfzo  15761  bitsmod  15762  gcdnncl  15833  gcd2n0cl  15835  qredeu  15979  cncongr2  15989  divnumden  16065  divdenle  16066  phisum  16104  pythagtriplem4  16133  pythagtriplem8  16137  pythagtriplem9  16138  isnsgrp  17883  isnmnd  17893  mgm2nsgrplem2  18062  0ringnnzr  20017  frlmssuvc2  20914  mamufacex  20975  mavmulsolcl  21135  maducoeval2  21224  opnfbas  22425  lgsneg  25883  numedglnl  26915  umgredgnlp  26918  umgr2edg1  26979  umgr2edgneu  26982  uhgrnbgr0nb  27122  nfrgr2v  28035  4cycl2vnunb  28053  hashxpe  30515  divnumden2  30520  fmlasucdisj  32653  poseq  33102  nodenselem8  33202  unbdqndv1  33854  relowlssretop  34660  relowlpssretop  34661  finxpreclem6  34693  itg2addnclem2  34987  elpadd0  36983  dihatlat  38508  dihjatcclem1  38592  rmspecnonsq  39643  rpnnen3lem  39767  gtnelicc  41928  xrgtnelicc  41966  limcrecl  42062  sumnnodd  42063  jumpncnp  42331  stoweidlem39  42472  stoweidlem59  42492  fourierdlem12  42552  preimagelt  43128  preimalegt  43129  pgrpgt2nabl  44559  lindslinindsimp1  44657  lmod1zrnlvec  44694  rrxsphere  44922
  Copyright terms: Public domain W3C validator