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 ⊢ (𝜑 → 𝜓)

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

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 210  df-an 401

This theorem is referenced by:  rlimcld2  15631  fincygsubgodd  20185  submomnd  20203  suborng  20960  ssdifidlprm  21467  perfectlem2  27372  2sqmod  27578  coltr  28899  prlngmo2  29184  ifnetrue  32871  nn0xmulclb  33094  dflringlem  33762  dflring3  33765  dflring4  33766  1arithufdlem3  33814  1arithufdlem4  33815  ballotlemfc0  34861  ballotlemic  34875  unbdqndv2lem1  37076  disjf1  45881  mapssbi  45909  supxrgere  46029  supxrgelem  46033  supxrge  46034  xrlexaddrp  46048  reclt0d  46082  uzn0bi  46153  eliccnelico  46225  qinioo  46231  iccdificc  46235  sqrlearg  46249  fsumsupp0  46274  limcrecl  46325  limsuppnflem  46404  climisp  46440  liminflbuz2  46509  climxlim2lem  46539  icccncfext  46581  stoweidlem52  46746  fourierdlem20  46821  fourierdlem34  46835  fourierdlem35  46836  fourierdlem38  46839  fourierdlem40  46841  fourierdlem41  46842  fourierdlem42  46843  fourierdlem46  46846  fourierdlem50  46850  fourierdlem60  46860  fourierdlem61  46861  fourierdlem64  46864  fourierdlem65  46865  fourierdlem72  46872  fourierdlem74  46874  fourierdlem75  46875  fourierdlem76  46876  fourierdlem78  46878  fouriersw  46925  elaa2lem  46927  etransclem24  46952  etransclem32  46960  etransclem35  46963  fge0iccico  47064  sge0cl  47075  sge0f1o  47076  sge0rernmpt  47116  meaiininclem  47180  hoidmv1lelem3  47287  hoidmvlelem2  47290  hoidmvlelem4  47292  hspmbllem2  47321  ovolval4lem1  47343  pimdecfgtioo  47411  pimincfltioo  47412  smfpimne2  47534  perfectALTVlem2  48464