Theorem condan 817

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

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

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 398

This theorem is referenced by:  rlimcld2  15522  fincygsubgodd  19982  perfectlem2  26733  2sqmod  26939  coltr  27898  ifnetrue  31779  nn0xmulclb  31984  submomnd  32228  suborng  32433  ballotlemfc0  33491  ballotlemic  33505  unbdqndv2lem1  35385  disjf1  43880  mapssbi  43912  supxrgere  44043  supxrgelem  44047  supxrge  44048  xrlexaddrp  44062  reclt0d  44097  uzn0bi  44169  eliccnelico  44242  qinioo  44248  iccdificc  44252  sqrlearg  44266  fsumsupp0  44294  limcrecl  44345  limsuppnflem  44426  climisp  44462  liminflbuz2  44531  climxlim2lem  44561  icccncfext  44603  stoweidlem52  44768  fourierdlem20  44843  fourierdlem34  44857  fourierdlem35  44858  fourierdlem38  44861  fourierdlem40  44863  fourierdlem41  44864  fourierdlem42  44865  fourierdlem46  44868  fourierdlem50  44872  fourierdlem60  44882  fourierdlem61  44883  fourierdlem64  44886  fourierdlem65  44887  fourierdlem72  44894  fourierdlem74  44896  fourierdlem75  44897  fourierdlem76  44898  fourierdlem78  44900  fouriersw  44947  elaa2lem  44949  etransclem24  44974  etransclem32  44982  etransclem35  44985  fge0iccico  45086  sge0cl  45097  sge0f1o  45098  sge0rernmpt  45138  meaiininclem  45202  hoidmv1lelem3  45309  hoidmvlelem2  45312  hoidmvlelem4  45314  hspmbllem2  45343  ovolval4lem1  45365  pimdecfgtioo  45433  pimincfltioo  45434  smfpimne2  45556  perfectALTVlem2  46390