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

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

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  14935  fincygsubgodd  19234  perfectlem2  25806  2sqmod  26012  coltr  26433  nn0xmulclb  30496  submomnd  30711  suborng  30888  ballotlemfc0  31750  ballotlemic  31764  unbdqndv2lem1  33848  disjf1  41463  mapssbi  41496  supxrgere  41621  supxrgelem  41625  supxrge  41626  xrlexaddrp  41640  reclt0d  41678  uzn0bi  41755  eliccnelico  41825  qinioo  41831  iccdificc  41835  sqrlearg  41849  fsumsupp0  41879  limcrecl  41930  limsuppnflem  42011  climisp  42047  liminflbuz2  42116  climxlim2lem  42146  icccncfext  42190  stoweidlem52  42357  fourierdlem20  42432  fourierdlem34  42446  fourierdlem35  42447  fourierdlem38  42450  fourierdlem40  42452  fourierdlem41  42453  fourierdlem42  42454  fourierdlem46  42457  fourierdlem50  42461  fourierdlem60  42471  fourierdlem61  42472  fourierdlem64  42475  fourierdlem65  42476  fourierdlem72  42483  fourierdlem74  42485  fourierdlem75  42486  fourierdlem76  42487  fourierdlem78  42489  fouriersw  42536  elaa2lem  42538  etransclem24  42563  etransclem32  42571  etransclem35  42574  fge0iccico  42672  sge0cl  42683  sge0f1o  42684  sge0rernmpt  42724  meaiininclem  42788  hoidmv1lelem3  42895  hoidmvlelem2  42898  hoidmvlelem4  42900  hspmbllem2  42929  ovolval4lem1  42951  pimdecfgtioo  43015  pimincfltioo  43016  perfectALTVlem2  43907