Theorem condan 829

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 828	. 2 ⊢ (𝜑 → ¬ ¬ 𝜓)
4	3	notnotrd 134	1 ⊢ (𝜑 → 𝜓)

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

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 210  df-an 401

This theorem is referenced by:  rlimcld2  15619  fincygsubgodd  20175  submomnd  20193  suborng  20948  ssdifidlprm  21446  perfectlem2  27352  2sqmod  27558  coltr  28875  ifnetrue  32803  nn0xmulclb  33028  dflringlem  33701  dflring3  33704  dflring4  33705  1arithufdlem3  33753  1arithufdlem4  33754  ballotlemfc0  34800  ballotlemic  34814  unbdqndv2lem1  36960  disjf1  45759  mapssbi  45787  supxrgere  45907  supxrgelem  45911  supxrge  45912  xrlexaddrp  45926  reclt0d  45960  uzn0bi  46031  eliccnelico  46103  qinioo  46109  iccdificc  46113  sqrlearg  46127  fsumsupp0  46152  limcrecl  46203  limsuppnflem  46282  climisp  46318  liminflbuz2  46387  climxlim2lem  46417  icccncfext  46459  stoweidlem52  46624  fourierdlem20  46699  fourierdlem34  46713  fourierdlem35  46714  fourierdlem38  46717  fourierdlem40  46719  fourierdlem41  46720  fourierdlem42  46721  fourierdlem46  46724  fourierdlem50  46728  fourierdlem60  46738  fourierdlem61  46739  fourierdlem64  46742  fourierdlem65  46743  fourierdlem72  46750  fourierdlem74  46752  fourierdlem75  46753  fourierdlem76  46754  fourierdlem78  46756  fouriersw  46803  elaa2lem  46805  etransclem24  46830  etransclem32  46838  etransclem35  46841  fge0iccico  46942  sge0cl  46953  sge0f1o  46954  sge0rernmpt  46994  meaiininclem  47058  hoidmv1lelem3  47165  hoidmvlelem2  47168  hoidmvlelem4  47170  hspmbllem2  47199  ovolval4lem1  47221  pimdecfgtioo  47289  pimincfltioo  47290  smfpimne2  47412  perfectALTVlem2  48342