Theorem condan 854

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

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

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 199  df-an 387

This theorem is referenced by:  rlimcld2  14687  perfectlem2  25369  coltr  25960  2sqmod  30194  submomnd  30256  suborng  30361  ballotlemfc0  31101  ballotlemic  31115  unbdqndv2lem1  33033  disjf1  40178  mapssbi  40212  supxrgere  40347  supxrgelem  40351  supxrge  40352  xrlexaddrp  40366  reclt0d  40405  uzn0bi  40484  eliccnelico  40552  qinioo  40558  iccdificc  40562  sqrlearg  40576  fsumsupp0  40606  limcrecl  40657  limsuppnflem  40738  climisp  40774  climxlim2lem  40867  icccncfext  40896  stoweidlem52  41064  fourierdlem20  41139  fourierdlem34  41153  fourierdlem35  41154  fourierdlem38  41157  fourierdlem40  41159  fourierdlem41  41160  fourierdlem42  41161  fourierdlem46  41164  fourierdlem50  41168  fourierdlem60  41178  fourierdlem61  41179  fourierdlem64  41182  fourierdlem65  41183  fourierdlem72  41190  fourierdlem74  41192  fourierdlem75  41193  fourierdlem76  41194  fourierdlem78  41196  fouriersw  41243  elaa2lem  41245  etransclem24  41270  etransclem32  41278  etransclem35  41281  fge0iccico  41379  sge0cl  41390  sge0f1o  41391  sge0rernmpt  41431  meaiininclem  41495  hoidmv1lelem3  41602  hoidmvlelem2  41605  hoidmvlelem4  41607  hspmbllem2  41636  ovolval4lem1  41658  pimdecfgtioo  41722  pimincfltioo  41723  perfectALTVlem2  42462