Theorem condan 829

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 400

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 401

This theorem is used by:  rlimcld2  15634  fincygsubgodd  20188  submomnd  20206  suborng  20988  ssdifidlprm  21495  perfectlem2  27403  2sqmod  27609  coltr  28930  prlngmo2  29215  ifnetrue  32902  nn0xmulclb  33125  dflringlem  33793  dflring3  33796  dflring4  33797  1arithufdlem3  33845  1arithufdlem4  33846  ballotlemfc0  34892  ballotlemic  34906  unbdqndv2lem1  37126  disjf1  45929  mapssbi  45957  supxrgere  46077  supxrgelem  46081  supxrge  46082  xrlexaddrp  46096  reclt0d  46130  uzn0bi  46201  eliccnelico  46273  qinioo  46279  iccdificc  46283  sqrlearg  46297  fsumsupp0  46322  limcrecl  46373  limsuppnflem  46452  climisp  46488  liminflbuz2  46557  climxlim2lem  46587  icccncfext  46629  stoweidlem52  46794  fourierdlem20  46869  fourierdlem34  46883  fourierdlem35  46884  fourierdlem38  46887  fourierdlem40  46889  fourierdlem41  46890  fourierdlem42  46891  fourierdlem46  46894  fourierdlem50  46898  fourierdlem60  46908  fourierdlem61  46909  fourierdlem64  46912  fourierdlem65  46913  fourierdlem72  46920  fourierdlem74  46922  fourierdlem75  46923  fourierdlem76  46924  fourierdlem78  46926  fouriersw  46973  elaa2lem  46975  etransclem24  47000  etransclem32  47008  etransclem35  47011  fge0iccico  47112  sge0cl  47123  sge0f1o  47124  sge0rernmpt  47164  meaiininclem  47228  hoidmv1lelem3  47335  hoidmvlelem2  47338  hoidmvlelem4  47340  hspmbllem2  47369  ovolval4lem1  47391  pimdecfgtioo  47459  pimincfltioo  47460  smfpimne2  47582  perfectALTVlem2  48515