Theorem condan 817

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 816	. 2 ⊢ (𝜑 → ¬ ¬ 𝜓)
4	3	notnotrd 135	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 210  df-an 400

This theorem is referenced by:  rlimcld2  14927  fincygsubgodd  19227  perfectlem2  25814  2sqmod  26020  coltr  26441  nn0xmulclb  30522  submomnd  30761  suborng  30939  ballotlemfc0  31860  ballotlemic  31874  unbdqndv2lem1  33961  disjf1  41809  mapssbi  41842  supxrgere  41965  supxrgelem  41969  supxrge  41970  xrlexaddrp  41984  reclt0d  42022  uzn0bi  42098  eliccnelico  42166  qinioo  42172  iccdificc  42176  sqrlearg  42190  fsumsupp0  42220  limcrecl  42271  limsuppnflem  42352  climisp  42388  liminflbuz2  42457  climxlim2lem  42487  icccncfext  42529  stoweidlem52  42694  fourierdlem20  42769  fourierdlem34  42783  fourierdlem35  42784  fourierdlem38  42787  fourierdlem40  42789  fourierdlem41  42790  fourierdlem42  42791  fourierdlem46  42794  fourierdlem50  42798  fourierdlem60  42808  fourierdlem61  42809  fourierdlem64  42812  fourierdlem65  42813  fourierdlem72  42820  fourierdlem74  42822  fourierdlem75  42823  fourierdlem76  42824  fourierdlem78  42826  fouriersw  42873  elaa2lem  42875  etransclem24  42900  etransclem32  42908  etransclem35  42911  fge0iccico  43009  sge0cl  43020  sge0f1o  43021  sge0rernmpt  43061  meaiininclem  43125  hoidmv1lelem3  43232  hoidmvlelem2  43235  hoidmvlelem4  43237  hspmbllem2  43266  ovolval4lem1  43288  pimdecfgtioo  43352  pimincfltioo  43353  perfectALTVlem2  44240