Theorem condan 830

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

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

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 402

This theorem is used by:  rlimcld2  15725  fincygsubgodd  20308  submomnd  20326  suborng  21113  ssdifidlprm  21622  perfectlem2  27539  2sqmod  27745  coltr  29098  prlngmo2  29416  ifnetrue  33125  nn0xmulclb  33345  dflringlem  34008  dflring3  34011  dflring4  34012  1arithufdlem3  34060  1arithufdlem4  34061  ballotlemfc0  35108  ballotlemic  35122  unbdqndv2lem1  37345  disjf1  46141  mapssbi  46169  supxrgere  46289  supxrgelem  46293  supxrge  46294  xrlexaddrp  46308  reclt0d  46342  uzn0bi  46413  eliccnelico  46485  qinioo  46491  iccdificc  46495  sqrlearg  46509  fsumsupp0  46534  limcrecl  46585  limsuppnflem  46664  climisp  46700  liminflbuz2  46769  climxlim2lem  46799  icccncfext  46841  stoweidlem52  47006  fourierdlem20  47081  fourierdlem34  47095  fourierdlem35  47096  fourierdlem38  47099  fourierdlem40  47101  fourierdlem41  47102  fourierdlem42  47103  fourierdlem46  47106  fourierdlem50  47110  fourierdlem60  47120  fourierdlem61  47121  fourierdlem64  47124  fourierdlem65  47125  fourierdlem72  47132  fourierdlem74  47134  fourierdlem75  47135  fourierdlem76  47136  fourierdlem78  47138  fouriersw  47185  elaa2lem  47187  etransclem24  47212  etransclem32  47220  etransclem35  47223  fge0iccico  47324  sge0cl  47335  sge0f1o  47336  sge0rernmpt  47376  meaiininclem  47440  hoidmv1lelem3  47547  hoidmvlelem2  47550  hoidmvlelem4  47552  hspmbllem2  47581  ovolval4lem1  47603  pimdecfgtioo  47671  pimincfltioo  47672  smfpimne2  47794  perfectALTVlem2  48764