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  15777  fincygsubgodd  20361  submomnd  20379  suborng  21166  ssdifidlprm  21675  perfectlem2  27590  2sqmod  27796  coltr  29149  prlngmo2  29467  ifnetrue  33218  nn0xmulclb  33436  dflringlem  34110  dflring3  34113  dflring4  34114  1arithufdlem3  34162  1arithufdlem4  34163  ballotlemfc0  35208  ballotlemic  35222  unbdqndv2lem1  37566  disjf1  46413  mapssbi  46441  supxrgere  46560  supxrgelem  46564  supxrge  46565  xrlexaddrp  46579  reclt0d  46613  uzn0bi  46684  eliccnelico  46756  qinioo  46762  iccdificc  46766  sqrlearg  46780  fsumsupp0  46805  limcrecl  46856  limsuppnflem  46935  climisp  46971  liminflbuz2  47040  climxlim2lem  47070  icccncfext  47112  stoweidlem52  47277  fourierdlem20  47352  fourierdlem34  47366  fourierdlem35  47367  fourierdlem38  47370  fourierdlem40  47372  fourierdlem41  47373  fourierdlem42  47374  fourierdlem46  47377  fourierdlem50  47381  fourierdlem60  47391  fourierdlem61  47392  fourierdlem64  47395  fourierdlem65  47396  fourierdlem72  47403  fourierdlem74  47405  fourierdlem75  47406  fourierdlem76  47407  fourierdlem78  47409  fouriersw  47456  elaa2lem  47458  etransclem24  47483  etransclem32  47491  etransclem35  47494  fge0iccico  47595  sge0cl  47606  sge0f1o  47607  sge0rernmpt  47647  meaiininclem  47711  hoidmv1lelem3  47818  hoidmvlelem2  47821  hoidmvlelem4  47823  hspmbllem2  47852  ovolval4lem1  47874  pimdecfgtioo  47942  pimincfltioo  47943  smfpimne2  48065  perfectALTVlem2  49035  parhomeqor2  50973  parhomeqor  50974