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

Theorem condan 852
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 599 . 2 (𝜑 → ¬ ¬ 𝜓)
43notnotrd 128 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:  rlimcld2  14353  perfectlem2  25000  coltr  25587  2sqmod  29776  submomnd  29838  suborng  29943  ballotlemfc0  30682  ballotlemic  30696  unbdqndv2lem1  32625  disjf1  39683  mapssbi  39719  supxrgere  39862  supxrgelem  39866  supxrge  39867  xrlexaddrp  39881  reclt0d  39920  uzn0bi  40002  eliccnelico  40074  qinioo  40080  iccdificc  40084  sqrlearg  40098  fsumsupp0  40128  limcrecl  40179  limsuppnflem  40260  climisp  40296  climxlim2lem  40389  icccncfext  40418  stoweidlem52  40587  fourierdlem20  40662  fourierdlem34  40676  fourierdlem35  40677  fourierdlem38  40680  fourierdlem40  40682  fourierdlem41  40683  fourierdlem42  40684  fourierdlem46  40687  fourierdlem50  40691  fourierdlem60  40701  fourierdlem61  40702  fourierdlem64  40705  fourierdlem65  40706  fourierdlem72  40713  fourierdlem74  40715  fourierdlem75  40716  fourierdlem76  40717  fourierdlem78  40719  fouriersw  40766  elaa2lem  40768  etransclem24  40793  etransclem32  40801  etransclem35  40804  fge0iccico  40905  sge0cl  40916  sge0f1o  40917  sge0rernmpt  40957  meaiininclem  41021  hoidmv1lelem3  41128  hoidmvlelem2  41131  hoidmvlelem4  41133  hspmbllem2  41162  ovolval4lem1  41184  pimdecfgtioo  41248  pimincfltioo  41249  perfectALTVlem2  41956
  Copyright terms: Public domain W3C validator