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

Theorem intnanrd 999
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 468 . 2 ((𝜓𝜒) → 𝜓)
31, 2nsyl 137 1 (𝜑 → ¬ (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 382
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 383
This theorem is referenced by:  bianfd  1003  3bior1fand  1587  pr1eqbg  4522  fvmptopab  6845  wemappo  8611  axrepnd  9619  axunnd  9621  fzpreddisj  12598  sadadd2lem2  15381  smumullem  15423  nndvdslegcd  15436  divgcdnn  15445  sqgcd  15487  coprm  15631  pythagtriplem19  15746  isnmnd  17507  nfimdetndef  20614  mdetfval1  20615  ibladdlem  23807  lgsval2lem  25254  lgsval4a  25266  lgsdilem  25271  nbgrnself  26479  wwlks  26964  iswspthsnon  26987  clwwlknclwwlkdifsOLD  27130  clwwlknon1nloop  27275  clwwlknon1le1  27277  nfrgr2v  27455  2sqcoprm  29988  nosepdmlem  32171  nodenselem8  32179  nosupbnd2lem1  32199  dfrdg4  32396  finxpreclem3  33568  finxpreclem5  33570  ibladdnclem  33799  dihatlat  37145  xppss12  37778  jm2.23  38090  ltnelicc  40241  limciccioolb  40372  dvmptfprodlem  40678  stoweidlem26  40761  fourierdlem12  40854  fourierdlem42  40884  divgcdoddALTV  42122
  Copyright terms: Public domain W3C validator