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

Theorem condan 831
 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 598 . 2 (𝜑 → ¬ ¬ 𝜓)
43notnotrd 127 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 196  df-an 385 This theorem is referenced by:  rlimcld2  14157  perfectlem2  24755  coltr  25342  2sqmod  28979  submomnd  29041  suborng  29146  ballotlemfc0  29881  ballotlemic  29895  unbdqndv2lem1  31670  disjf1  38364  mapssbi  38400  supxrgere  38490  supxrgelem  38494  supxrge  38495  xrlexaddrp  38509  reclt0d  38548  eliccnelico  38603  qinioo  38609  iccdificc  38613  sqrlearg  38627  fsumsupp0  38645  limcrecl  38696  icccncfext  38773  stoweidlem52  38945  fourierdlem20  39020  fourierdlem34  39034  fourierdlem35  39035  fourierdlem38  39038  fourierdlem40  39040  fourierdlem41  39041  fourierdlem42  39042  fourierdlem46  39045  fourierdlem50  39049  fourierdlem60  39059  fourierdlem61  39060  fourierdlem64  39063  fourierdlem65  39064  fourierdlem72  39071  fourierdlem74  39073  fourierdlem75  39074  fourierdlem76  39075  fourierdlem78  39077  fouriersw  39124  elaa2lem  39126  etransclem24  39151  etransclem32  39159  etransclem35  39162  fge0iccico  39263  sge0cl  39274  sge0f1o  39275  sge0rernmpt  39315  meaiininclem  39376  hoidmv1lelem3  39483  hoidmvlelem2  39486  hoidmvlelem4  39488  hspmbllem2  39517  ovolval4lem1  39539  pimdecfgtioo  39604  pimincfltioo  39605  perfectALTVlem2  40165
 Copyright terms: Public domain W3C validator