Theorem condan 815

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

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

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 206  df-an 397

This theorem is referenced by:  rlimcld2  15287  fincygsubgodd  19715  perfectlem2  26378  2sqmod  26584  coltr  27008  nn0xmulclb  31094  submomnd  31336  suborng  31514  ballotlemfc0  32459  ballotlemic  32473  unbdqndv2lem1  34689  disjf1  42720  mapssbi  42753  supxrgere  42872  supxrgelem  42876  supxrge  42877  xrlexaddrp  42891  reclt0d  42926  uzn0bi  42999  eliccnelico  43067  qinioo  43073  iccdificc  43077  sqrlearg  43091  fsumsupp0  43119  limcrecl  43170  limsuppnflem  43251  climisp  43287  liminflbuz2  43356  climxlim2lem  43386  icccncfext  43428  stoweidlem52  43593  fourierdlem20  43668  fourierdlem34  43682  fourierdlem35  43683  fourierdlem38  43686  fourierdlem40  43688  fourierdlem41  43689  fourierdlem42  43690  fourierdlem46  43693  fourierdlem50  43697  fourierdlem60  43707  fourierdlem61  43708  fourierdlem64  43711  fourierdlem65  43712  fourierdlem72  43719  fourierdlem74  43721  fourierdlem75  43722  fourierdlem76  43723  fourierdlem78  43725  fouriersw  43772  elaa2lem  43774  etransclem24  43799  etransclem32  43807  etransclem35  43810  fge0iccico  43908  sge0cl  43919  sge0f1o  43920  sge0rernmpt  43960  meaiininclem  44024  hoidmv1lelem3  44131  hoidmvlelem2  44134  hoidmvlelem4  44136  hspmbllem2  44165  ovolval4lem1  44187  pimdecfgtioo  44254  pimincfltioo  44255  perfectALTVlem2  45174