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

Theorem condan 830
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 597 . 2 (𝜑 → ¬ ¬ 𝜓)
43notnotrd 126 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 382
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 195  df-an 384
This theorem is referenced by:  rlimcld2  14103  perfectlem2  24672  coltr  25260  2sqmod  28785  submomnd  28847  suborng  28952  ballotlemfc0  29687  ballotlemic  29701  unbdqndv2lem1  31476  disjf1  38167  mapssbi  38203  supxrgere  38294  supxrgelem  38298  supxrge  38299  xrlexaddrp  38313  reclt0d  38352  eliccnelico  38407  qinioo  38413  iccdificc  38417  sqrlearg  38431  fsumsupp0  38449  limcrecl  38500  icccncfext  38577  stoweidlem52  38749  fourierdlem20  38824  fourierdlem34  38838  fourierdlem35  38839  fourierdlem38  38842  fourierdlem40  38844  fourierdlem41  38845  fourierdlem42  38846  fourierdlem46  38849  fourierdlem50  38853  fourierdlem60  38863  fourierdlem61  38864  fourierdlem64  38867  fourierdlem65  38868  fourierdlem72  38875  fourierdlem74  38877  fourierdlem75  38878  fourierdlem76  38879  fourierdlem78  38881  fouriersw  38928  elaa2lem  38930  etransclem24  38955  etransclem32  38963  etransclem35  38966  fge0iccico  39067  sge0cl  39078  sge0f1o  39079  sge0rernmpt  39119  meaiininclem  39180  hoidmv1lelem3  39287  hoidmvlelem2  39290  hoidmvlelem4  39292  hspmbllem2  39321  ovolval4lem1  39343  pimdecfgtioo  39408  pimincfltioo  39409  perfectALTVlem2  39970
  Copyright terms: Public domain W3C validator