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

Theorem intnanrd 962
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 473 . 2 ((𝜓𝜒) → 𝜓)
31, 2nsyl 135 1 (𝜑 → ¬ (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 384
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 386
This theorem is referenced by:  bianfd  966  3bior1fand  1436  pr1eqbg  4358  fvmptopab  6650  wemappo  8398  axrepnd  9360  axunnd  9362  fzpreddisj  12332  sadadd2lem2  15096  smumullem  15138  nndvdslegcd  15151  divgcdnn  15160  sqgcd  15202  divgcdodd  15346  coprm  15347  pythagtriplem19  15462  isnmnd  17219  nfimdetndef  20314  mdetfval1  20315  ibladdlem  23492  lgsval2lem  24932  lgsval4a  24944  lgsdilem  24949  nbgrnself  26144  wwlks  26596  clwwlknclwwlkdifs  26740  nfrgr2v  27000  2sqcoprm  29429  nodenselem8  31548  nosepdmlem  31564  dfrdg4  31697  finxpreclem3  32859  finxpreclem5  32861  ibladdnclem  33095  dihatlat  36100  jm2.23  37040  ltnelicc  39127  limciccioolb  39254  dvmptfprodlem  39462  stoweidlem26  39547  fourierdlem12  39640  fourierdlem42  39670  divgcdoddALTV  40889
  Copyright terms: Public domain W3C validator