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

Theorem intnanrd 491
Description: Introduction of conjunct inside of a contradiction. (Contributed by NM, 10-Jul-2005.)
Hypothesis
Ref Expression
intnand.1 (𝜑 → ¬ 𝜓)
Assertion
Ref Expression
intnanrd (𝜑 → ¬ (𝜓𝜒))

Proof of Theorem intnanrd
StepHypRef Expression
1 intnand.1 . 2 (𝜑 → ¬ 𝜓)
2 simpl 484 . 2 ((𝜓𝜒) → 𝜓)
31, 2nsyl 140 1 (𝜑 → ¬ (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 397
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 206  df-an 398
This theorem is referenced by:  bianfd  536  3bior1fand  1477  pr1eqbg  4819  iresn0n0  6012  fvmptopabOLD  7417  frxp2  8081  frxp3  8088  wemappo  9492  axrepnd  10537  axunnd  10539  fzpreddisj  13497  sadadd2lem2  16337  smumullem  16379  nndvdslegcd  16392  divgcdnn  16402  sqgcd  16448  coprm  16594  isnmnd  18567  nfimdetndef  21954  mdetfval1  21955  ibladdlem  25200  lgsval2lem  26671  lgsval4a  26683  lgsdilem  26688  2sqcoprm  26799  addsqn2reurex2  26809  nosepdmlem  27047  nodenselem8  27055  nosupbnd2lem1  27079  nbgrnself  28349  wwlks  28822  iswspthsnon  28843  clwwlknon1nloop  29085  clwwlknon1le1  29087  nfrgr2v  29258  hashxpe  31751  acycgr0v  33782  prclisacycgr  33785  fmlasucdisj  34033  dfrdg4  34565  finxpreclem3  35893  finxpreclem5  35895  ibladdnclem  36163  dihatlat  39826  xppss12  40681  jm2.23  41349  rexanuz2nf  43802  ltnelicc  43809  limciccioolb  43936  dvmptfprodlem  44259  stoweidlem26  44341  fourierdlem12  44434  fourierdlem42  44464  divgcdoddALTV  45948
  Copyright terms: Public domain W3C validator