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 133	1 ⊢ (𝜑 → 𝜓)

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

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 398

This theorem is referenced by:  rlimcld2  15522  fincygsubgodd  19982  perfectlem2  26733  2sqmod  26939  coltr  27929  ifnetrue  31810  nn0xmulclb  32015  submomnd  32259  suborng  32464  ballotlemfc0  33522  ballotlemic  33536  unbdqndv2lem1  35433  disjf1  43928  mapssbi  43960  supxrgere  44091  supxrgelem  44095  supxrge  44096  xrlexaddrp  44110  reclt0d  44145  uzn0bi  44217  eliccnelico  44290  qinioo  44296  iccdificc  44300  sqrlearg  44314  fsumsupp0  44342  limcrecl  44393  limsuppnflem  44474  climisp  44510  liminflbuz2  44579  climxlim2lem  44609  icccncfext  44651  stoweidlem52  44816  fourierdlem20  44891  fourierdlem34  44905  fourierdlem35  44906  fourierdlem38  44909  fourierdlem40  44911  fourierdlem41  44912  fourierdlem42  44913  fourierdlem46  44916  fourierdlem50  44920  fourierdlem60  44930  fourierdlem61  44931  fourierdlem64  44934  fourierdlem65  44935  fourierdlem72  44942  fourierdlem74  44944  fourierdlem75  44945  fourierdlem76  44946  fourierdlem78  44948  fouriersw  44995  elaa2lem  44997  etransclem24  45022  etransclem32  45030  etransclem35  45033  fge0iccico  45134  sge0cl  45145  sge0f1o  45146  sge0rernmpt  45186  meaiininclem  45250  hoidmv1lelem3  45357  hoidmvlelem2  45360  hoidmvlelem4  45362  hspmbllem2  45391  ovolval4lem1  45413  pimdecfgtioo  45481  pimincfltioo  45482  smfpimne2  45604  perfectALTVlem2  46438