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

Theorem intnanrd 490
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 483 . 2 ((𝜓𝜒) → 𝜓)
31, 2nsyl 142 1 (𝜑 → ¬ (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396
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 208  df-an 397
This theorem is referenced by:  bianfd  535  3bior1fand  1467  pr1eqbg  4779  iresn0n0  5916  fvmptopab  7198  wemappo  9001  axrepnd  10004  axunnd  10006  fzpreddisj  12944  sadadd2lem2  15787  smumullem  15829  nndvdslegcd  15842  divgcdnn  15851  sqgcd  15897  coprm  16043  isnmnd  17903  nfimdetndef  21126  mdetfval1  21127  ibladdlem  24347  lgsval2lem  25810  lgsval4a  25822  lgsdilem  25827  2sqcoprm  25938  addsqn2reurex2  25948  nbgrnself  27068  wwlks  27540  iswspthsnon  27561  clwwlknon1nloop  27805  clwwlknon1le1  27807  nfrgr2v  27978  hashxpe  30455  acycgr0v  32292  prclisacycgr  32295  fmlasucdisj  32543  nosepdmlem  33084  nodenselem8  33092  nosupbnd2lem1  33112  dfrdg4  33309  finxpreclem3  34556  finxpreclem5  34558  ibladdnclem  34829  dihatlat  38350  xppss12  38993  jm2.23  39471  ltnelicc  41648  limciccioolb  41778  dvmptfprodlem  42105  stoweidlem26  42188  fourierdlem12  42281  fourierdlem42  42311  divgcdoddALTV  43724
  Copyright terms: Public domain W3C validator