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

Theorem condan 816
 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 815 . 2 (𝜑 → ¬ ¬ 𝜓)
43notnotrd 135 1 (𝜑𝜓)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 398 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 209  df-an 399 This theorem is referenced by:  rlimcld2  14915  fincygsubgodd  19213  perfectlem2  25793  2sqmod  25999  coltr  26420  nn0xmulclb  30483  submomnd  30719  suborng  30896  ballotlemfc0  31758  ballotlemic  31772  unbdqndv2lem1  33856  disjf1  41597  mapssbi  41630  supxrgere  41755  supxrgelem  41759  supxrge  41760  xrlexaddrp  41774  reclt0d  41812  uzn0bi  41889  eliccnelico  41957  qinioo  41963  iccdificc  41967  sqrlearg  41981  fsumsupp0  42011  limcrecl  42062  limsuppnflem  42143  climisp  42179  liminflbuz2  42248  climxlim2lem  42278  icccncfext  42320  stoweidlem52  42485  fourierdlem20  42560  fourierdlem34  42574  fourierdlem35  42575  fourierdlem38  42578  fourierdlem40  42580  fourierdlem41  42581  fourierdlem42  42582  fourierdlem46  42585  fourierdlem50  42589  fourierdlem60  42599  fourierdlem61  42600  fourierdlem64  42603  fourierdlem65  42604  fourierdlem72  42611  fourierdlem74  42613  fourierdlem75  42614  fourierdlem76  42615  fourierdlem78  42617  fouriersw  42664  elaa2lem  42666  etransclem24  42691  etransclem32  42699  etransclem35  42702  fge0iccico  42800  sge0cl  42811  sge0f1o  42812  sge0rernmpt  42852  meaiininclem  42916  hoidmv1lelem3  43023  hoidmvlelem2  43026  hoidmvlelem4  43028  hspmbllem2  43057  ovolval4lem1  43079  pimdecfgtioo  43143  pimincfltioo  43144  perfectALTVlem2  44032
 Copyright terms: Public domain W3C validator