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

Theorem condan 817
Description: Proof by contradiction. (Contributed by NM, 9-Feb-2006.) (Proof shortened by Wolf Lammen, 19-Jun-2014.)
Hypotheses
Ref Expression
condan.1 ((𝜑 ∧ ¬ 𝜓) → 𝜒)
condan.2 ((𝜑 ∧ ¬ 𝜓) → ¬ 𝜒)
Assertion
Ref Expression
condan (𝜑𝜓)

Proof of Theorem condan
StepHypRef Expression
1 condan.1 . . 3 ((𝜑 ∧ ¬ 𝜓) → 𝜒)
2 condan.2 . . 3 ((𝜑 ∧ ¬ 𝜓) → ¬ 𝜒)
31, 2pm2.65da 816 . 2 (𝜑 → ¬ ¬ 𝜓)
43notnotrd 133 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 397
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 206  df-an 398
This theorem is referenced by:  rlimcld2  15467  fincygsubgodd  19898  perfectlem2  26594  2sqmod  26800  coltr  27631  nn0xmulclb  31718  submomnd  31960  suborng  32150  ballotlemfc0  33132  ballotlemic  33146  unbdqndv2lem1  35001  disjf1  43475  mapssbi  43508  supxrgere  43641  supxrgelem  43645  supxrge  43646  xrlexaddrp  43660  reclt0d  43695  uzn0bi  43768  eliccnelico  43841  qinioo  43847  iccdificc  43851  sqrlearg  43865  fsumsupp0  43893  limcrecl  43944  limsuppnflem  44025  climisp  44061  liminflbuz2  44130  climxlim2lem  44160  icccncfext  44202  stoweidlem52  44367  fourierdlem20  44442  fourierdlem34  44456  fourierdlem35  44457  fourierdlem38  44460  fourierdlem40  44462  fourierdlem41  44463  fourierdlem42  44464  fourierdlem46  44467  fourierdlem50  44471  fourierdlem60  44481  fourierdlem61  44482  fourierdlem64  44485  fourierdlem65  44486  fourierdlem72  44493  fourierdlem74  44495  fourierdlem75  44496  fourierdlem76  44497  fourierdlem78  44499  fouriersw  44546  elaa2lem  44548  etransclem24  44573  etransclem32  44581  etransclem35  44584  fge0iccico  44685  sge0cl  44696  sge0f1o  44697  sge0rernmpt  44737  meaiininclem  44801  hoidmv1lelem3  44908  hoidmvlelem2  44911  hoidmvlelem4  44913  hspmbllem2  44942  ovolval4lem1  44964  pimdecfgtioo  45032  pimincfltioo  45033  smfpimne2  45155  perfectALTVlem2  45988
  Copyright terms: Public domain W3C validator