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

Theorem condan 818
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 817 . 2 (𝜑 → ¬ ¬ 𝜓)
43notnotrd 133 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 395
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 207  df-an 396
This theorem is referenced by:  rlimcld2  15614  fincygsubgodd  20132  perfectlem2  27274  2sqmod  27480  coltr  28655  ifnetrue  32560  nn0xmulclb  32775  submomnd  33087  suborng  33345  ssdifidlprm  33486  1arithufdlem3  33574  1arithufdlem4  33575  ballotlemfc0  34495  ballotlemic  34509  unbdqndv2lem1  36510  disjf1  45188  mapssbi  45218  supxrgere  45344  supxrgelem  45348  supxrge  45349  xrlexaddrp  45363  reclt0d  45398  uzn0bi  45470  eliccnelico  45542  qinioo  45548  iccdificc  45552  sqrlearg  45566  fsumsupp0  45593  limcrecl  45644  limsuppnflem  45725  climisp  45761  liminflbuz2  45830  climxlim2lem  45860  icccncfext  45902  stoweidlem52  46067  fourierdlem20  46142  fourierdlem34  46156  fourierdlem35  46157  fourierdlem38  46160  fourierdlem40  46162  fourierdlem41  46163  fourierdlem42  46164  fourierdlem46  46167  fourierdlem50  46171  fourierdlem60  46181  fourierdlem61  46182  fourierdlem64  46185  fourierdlem65  46186  fourierdlem72  46193  fourierdlem74  46195  fourierdlem75  46196  fourierdlem76  46197  fourierdlem78  46199  fouriersw  46246  elaa2lem  46248  etransclem24  46273  etransclem32  46281  etransclem35  46284  fge0iccico  46385  sge0cl  46396  sge0f1o  46397  sge0rernmpt  46437  meaiininclem  46501  hoidmv1lelem3  46608  hoidmvlelem2  46611  hoidmvlelem4  46613  hspmbllem2  46642  ovolval4lem1  46664  pimdecfgtioo  46732  pimincfltioo  46733  smfpimne2  46855  perfectALTVlem2  47709
  Copyright terms: Public domain W3C validator