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  15285  fincygsubgodd  19713  perfectlem2  26376  2sqmod  26582  coltr  27006  nn0xmulclb  31091  submomnd  31333  suborng  31511  ballotlemfc0  32456  ballotlemic  32470  unbdqndv2lem1  34686  disjf1  42690  mapssbi  42723  supxrgere  42842  supxrgelem  42846  supxrge  42847  xrlexaddrp  42861  reclt0d  42896  uzn0bi  42969  eliccnelico  43037  qinioo  43043  iccdificc  43047  sqrlearg  43061  fsumsupp0  43089  limcrecl  43140  limsuppnflem  43221  climisp  43257  liminflbuz2  43326  climxlim2lem  43356  icccncfext  43398  stoweidlem52  43563  fourierdlem20  43638  fourierdlem34  43652  fourierdlem35  43653  fourierdlem38  43656  fourierdlem40  43658  fourierdlem41  43659  fourierdlem42  43660  fourierdlem46  43663  fourierdlem50  43667  fourierdlem60  43677  fourierdlem61  43678  fourierdlem64  43681  fourierdlem65  43682  fourierdlem72  43689  fourierdlem74  43691  fourierdlem75  43692  fourierdlem76  43693  fourierdlem78  43695  fouriersw  43742  elaa2lem  43744  etransclem24  43769  etransclem32  43777  etransclem35  43780  fge0iccico  43878  sge0cl  43889  sge0f1o  43890  sge0rernmpt  43930  meaiininclem  43994  hoidmv1lelem3  44101  hoidmvlelem2  44104  hoidmvlelem4  44106  hspmbllem2  44135  ovolval4lem1  44157  pimdecfgtioo  44221  pimincfltioo  44222  perfectALTVlem2  45141