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

Theorem intnanrd 954
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 472 . 2 ((𝜓𝜒) → 𝜓)
31, 2nsyl 134 1 (𝜑 → ¬ (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 383
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 196  df-an 385
This theorem is referenced by:  bianfd  963  3bior1fand  1431  wemappo  8337  axrepnd  9295  axunnd  9297  fzpreddisj  12260  sadadd2lem2  15010  smumullem  15052  nndvdslegcd  15065  divgcdnn  15074  sqgcd  15116  divgcdodd  15260  coprm  15261  pythagtriplem19  15376  isnmnd  17121  nfimdetndef  20214  mdetfval1  20215  ibladdlem  23392  lgsval2lem  24832  lgsval4a  24844  lgsdilem  24849  uvtx01vtx  26020  clwlknclwlkdifs  26487  frgra2v  26526  2sqcoprm  28978  nodenselem8  31087  dfrdg4  31228  finxpreclem3  32406  finxpreclem5  32408  ibladdnclem  32636  dihatlat  35641  jm2.23  36581  ltnelicc  38566  limciccioolb  38688  dvmptfprodlem  38834  stoweidlem26  38919  fourierdlem12  39012  fourierdlem42  39042  divgcdoddALTV  40131  pr1eqbg  40313  nbgrnself  40583  wwlks  41038  clwwlknclwwlkdifs  41181  nfrgr2v  41442
  Copyright terms: Public domain W3C validator