Theorem condan 814

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

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

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 396

This theorem is referenced by:  rlimcld2  15215  fincygsubgodd  19630  perfectlem2  26283  2sqmod  26489  coltr  26912  nn0xmulclb  30996  submomnd  31238  suborng  31416  ballotlemfc0  32359  ballotlemic  32373  unbdqndv2lem1  34616  disjf1  42609  mapssbi  42642  supxrgere  42762  supxrgelem  42766  supxrge  42767  xrlexaddrp  42781  reclt0d  42816  uzn0bi  42889  eliccnelico  42957  qinioo  42963  iccdificc  42967  sqrlearg  42981  fsumsupp0  43009  limcrecl  43060  limsuppnflem  43141  climisp  43177  liminflbuz2  43246  climxlim2lem  43276  icccncfext  43318  stoweidlem52  43483  fourierdlem20  43558  fourierdlem34  43572  fourierdlem35  43573  fourierdlem38  43576  fourierdlem40  43578  fourierdlem41  43579  fourierdlem42  43580  fourierdlem46  43583  fourierdlem50  43587  fourierdlem60  43597  fourierdlem61  43598  fourierdlem64  43601  fourierdlem65  43602  fourierdlem72  43609  fourierdlem74  43611  fourierdlem75  43612  fourierdlem76  43613  fourierdlem78  43615  fouriersw  43662  elaa2lem  43664  etransclem24  43689  etransclem32  43697  etransclem35  43700  fge0iccico  43798  sge0cl  43809  sge0f1o  43810  sge0rernmpt  43850  meaiininclem  43914  hoidmv1lelem3  44021  hoidmvlelem2  44024  hoidmvlelem4  44026  hspmbllem2  44055  ovolval4lem1  44077  pimdecfgtioo  44141  pimincfltioo  44142  perfectALTVlem2  45062