Theorem condan 816

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 815	. 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  15472  fincygsubgodd  19905  perfectlem2  26615  2sqmod  26821  coltr  27652  ifnetrue  31533  nn0xmulclb  31744  submomnd  31988  suborng  32181  ballotlemfc0  33181  ballotlemic  33195  unbdqndv2lem1  35048  disjf1  43523  mapssbi  43555  supxrgere  43688  supxrgelem  43692  supxrge  43693  xrlexaddrp  43707  reclt0d  43742  uzn0bi  43814  eliccnelico  43887  qinioo  43893  iccdificc  43897  sqrlearg  43911  fsumsupp0  43939  limcrecl  43990  limsuppnflem  44071  climisp  44107  liminflbuz2  44176  climxlim2lem  44206  icccncfext  44248  stoweidlem52  44413  fourierdlem20  44488  fourierdlem34  44502  fourierdlem35  44503  fourierdlem38  44506  fourierdlem40  44508  fourierdlem41  44509  fourierdlem42  44510  fourierdlem46  44513  fourierdlem50  44517  fourierdlem60  44527  fourierdlem61  44528  fourierdlem64  44531  fourierdlem65  44532  fourierdlem72  44539  fourierdlem74  44541  fourierdlem75  44542  fourierdlem76  44543  fourierdlem78  44545  fouriersw  44592  elaa2lem  44594  etransclem24  44619  etransclem32  44627  etransclem35  44630  fge0iccico  44731  sge0cl  44742  sge0f1o  44743  sge0rernmpt  44783  meaiininclem  44847  hoidmv1lelem3  44954  hoidmvlelem2  44957  hoidmvlelem4  44959  hspmbllem2  44988  ovolval4lem1  45010  pimdecfgtioo  45078  pimincfltioo  45079  smfpimne2  45201  perfectALTVlem2  46034