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 394

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 395

This theorem is referenced by:  rlimcld2  15562  fincygsubgodd  20076  perfectlem2  27183  2sqmod  27389  coltr  28471  ifnetrue  32359  nn0xmulclb  32562  submomnd  32811  suborng  33054  ballotlemfc0  34145  ballotlemic  34159  unbdqndv2lem1  36017  disjf1  44586  mapssbi  44616  supxrgere  44744  supxrgelem  44748  supxrge  44749  xrlexaddrp  44763  reclt0d  44798  uzn0bi  44870  eliccnelico  44943  qinioo  44949  iccdificc  44953  sqrlearg  44967  fsumsupp0  44995  limcrecl  45046  limsuppnflem  45127  climisp  45163  liminflbuz2  45232  climxlim2lem  45262  icccncfext  45304  stoweidlem52  45469  fourierdlem20  45544  fourierdlem34  45558  fourierdlem35  45559  fourierdlem38  45562  fourierdlem40  45564  fourierdlem41  45565  fourierdlem42  45566  fourierdlem46  45569  fourierdlem50  45573  fourierdlem60  45583  fourierdlem61  45584  fourierdlem64  45587  fourierdlem65  45588  fourierdlem72  45595  fourierdlem74  45597  fourierdlem75  45598  fourierdlem76  45599  fourierdlem78  45601  fouriersw  45648  elaa2lem  45650  etransclem24  45675  etransclem32  45683  etransclem35  45686  fge0iccico  45787  sge0cl  45798  sge0f1o  45799  sge0rernmpt  45839  meaiininclem  45903  hoidmv1lelem3  46010  hoidmvlelem2  46013  hoidmvlelem4  46015  hspmbllem2  46044  ovolval4lem1  46066  pimdecfgtioo  46134  pimincfltioo  46135  smfpimne2  46257  perfectALTVlem2  47091