Theorem condan 827

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

Step	Hyp	Ref	Expression
1		condan.1	. . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝜒)
2		condan.2	. . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → ¬ 𝜒)
3	1, 2	pm2.65da 826	. 2 ⊢ (𝜑 → ¬ ¬ 𝜓)
4	3	notnotrd 133	1 ⊢ (𝜑 → 𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399

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 400

This theorem is referenced by:  rlimcld2  15588  fincygsubgodd  20137  submomnd  20155  suborng  20905  perfectlem2  27271  2sqmod  27477  coltr  28793  ifnetrue  32695  nn0xmulclb  32923  ssdifidlprm  33606  dflringlem  33651  dflring3  33654  dflring4  33655  1arithufdlem3  33703  1arithufdlem4  33704  ballotlemfc0  34751  ballotlemic  34765  unbdqndv2lem1  36911  disjf1  45725  mapssbi  45753  supxrgere  45873  supxrgelem  45877  supxrge  45878  xrlexaddrp  45892  reclt0d  45926  uzn0bi  45997  eliccnelico  46069  qinioo  46075  iccdificc  46079  sqrlearg  46093  fsumsupp0  46118  limcrecl  46169  limsuppnflem  46248  climisp  46284  liminflbuz2  46353  climxlim2lem  46383  icccncfext  46425  stoweidlem52  46590  fourierdlem20  46665  fourierdlem34  46679  fourierdlem35  46680  fourierdlem38  46683  fourierdlem40  46685  fourierdlem41  46686  fourierdlem42  46687  fourierdlem46  46690  fourierdlem50  46694  fourierdlem60  46704  fourierdlem61  46705  fourierdlem64  46708  fourierdlem65  46709  fourierdlem72  46716  fourierdlem74  46718  fourierdlem75  46719  fourierdlem76  46720  fourierdlem78  46722  fouriersw  46769  elaa2lem  46771  etransclem24  46796  etransclem32  46804  etransclem35  46807  fge0iccico  46908  sge0cl  46919  sge0f1o  46920  sge0rernmpt  46960  meaiininclem  47024  hoidmv1lelem3  47131  hoidmvlelem2  47134  hoidmvlelem4  47136  hspmbllem2  47165  ovolval4lem1  47187  pimdecfgtioo  47255  pimincfltioo  47256  smfpimne2  47378  perfectALTVlem2  48308