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

Theorem intnanrd 493
 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 486 . 2 ((𝜓𝜒) → 𝜓)
31, 2nsyl 142 1 (𝜑 → ¬ (𝜓𝜒))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399 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 210  df-an 400 This theorem is referenced by:  bianfd  538  3bior1fand  1473  pr1eqbg  4747  iresn0n0  5890  fvmptopab  7188  wemappo  8999  axrepnd  10007  axunnd  10009  fzpreddisj  12953  sadadd2lem2  15791  smumullem  15833  nndvdslegcd  15846  divgcdnn  15855  sqgcd  15901  coprm  16047  isnmnd  17909  nfimdetndef  21201  mdetfval1  21202  ibladdlem  24430  lgsval2lem  25898  lgsval4a  25910  lgsdilem  25915  2sqcoprm  26026  addsqn2reurex2  26036  nbgrnself  27156  wwlks  27628  iswspthsnon  27649  clwwlknon1nloop  27891  clwwlknon1le1  27893  nfrgr2v  28064  hashxpe  30562  acycgr0v  32520  prclisacycgr  32523  fmlasucdisj  32771  nosepdmlem  33312  nodenselem8  33320  nosupbnd2lem1  33340  dfrdg4  33537  finxpreclem3  34826  finxpreclem5  34828  ibladdnclem  35129  dihatlat  38646  xppss12  39425  jm2.23  39952  ltnelicc  42149  limciccioolb  42278  dvmptfprodlem  42601  stoweidlem26  42683  fourierdlem12  42776  fourierdlem42  42806  divgcdoddALTV  44215
 Copyright terms: Public domain W3C validator