Theorem condan 830

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  rlimcld2  15655  fincygsubgodd  20215  submomnd  20233  suborng  21016  ssdifidlprm  21523  perfectlem2  27431  2sqmod  27637  coltr  28958  prlngmo2  29243  ifnetrue  32930  nn0xmulclb  33153  dflringlem  33815  dflring3  33818  dflring4  33819  1arithufdlem3  33867  1arithufdlem4  33868  ballotlemfc0  34915  ballotlemic  34929  unbdqndv2lem1  37139  disjf1  45942  mapssbi  45970  supxrgere  46090  supxrgelem  46094  supxrge  46095  xrlexaddrp  46109  reclt0d  46143  uzn0bi  46214  eliccnelico  46286  qinioo  46292  iccdificc  46296  sqrlearg  46310  fsumsupp0  46335  limcrecl  46386  limsuppnflem  46465  climisp  46501  liminflbuz2  46570  climxlim2lem  46600  icccncfext  46642  stoweidlem52  46807  fourierdlem20  46882  fourierdlem34  46896  fourierdlem35  46897  fourierdlem38  46900  fourierdlem40  46902  fourierdlem41  46903  fourierdlem42  46904  fourierdlem46  46907  fourierdlem50  46911  fourierdlem60  46921  fourierdlem61  46922  fourierdlem64  46925  fourierdlem65  46926  fourierdlem72  46933  fourierdlem74  46935  fourierdlem75  46936  fourierdlem76  46937  fourierdlem78  46939  fouriersw  46986  elaa2lem  46988  etransclem24  47013  etransclem32  47021  etransclem35  47024  fge0iccico  47125  sge0cl  47136  sge0f1o  47137  sge0rernmpt  47177  meaiininclem  47241  hoidmv1lelem3  47348  hoidmvlelem2  47351  hoidmvlelem4  47353  hspmbllem2  47382  ovolval4lem1  47404  pimdecfgtioo  47472  pimincfltioo  47473  smfpimne2  47595  perfectALTVlem2  48528