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

Theorem intnanrd 983
 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 135 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 197  df-an 385 This theorem is referenced by:  bianfd  987  3bior1fand  1479  pr1eqbg  4421  fvmptopab  6739  wemappo  8495  axrepnd  9454  axunnd  9456  fzpreddisj  12428  sadadd2lem2  15219  smumullem  15261  nndvdslegcd  15274  divgcdnn  15283  sqgcd  15325  coprm  15470  pythagtriplem19  15585  isnmnd  17345  nfimdetndef  20443  mdetfval1  20444  ibladdlem  23631  lgsval2lem  25077  lgsval4a  25089  lgsdilem  25094  nbgrnself  26300  wwlks  26783  iswspthsnon  26806  clwwlknclwwlkdifsOLD  26947  clwwlknon1nloop  27074  clwwlknon1le1  27076  nfrgr2v  27252  2sqcoprm  29775  nosepdmlem  31958  nodenselem8  31966  nosupbnd2lem1  31986  dfrdg4  32183  finxpreclem3  33360  finxpreclem5  33362  ibladdnclem  33596  dihatlat  36940  jm2.23  37880  ltnelicc  40037  limciccioolb  40171  dvmptfprodlem  40477  stoweidlem26  40561  fourierdlem12  40654  fourierdlem42  40684  divgcdoddALTV  41918
 Copyright terms: Public domain W3C validator