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  15669  fincygsubgodd  20247  submomnd  20265  suborng  21048  ssdifidlprm  21555  perfectlem2  27474  2sqmod  27680  coltr  29003  prlngmo2  29321  ifnetrue  33030  nn0xmulclb  33250  dflringlem  33912  dflring3  33915  dflring4  33916  1arithufdlem3  33964  1arithufdlem4  33965  ballotlemfc0  35012  ballotlemic  35026  unbdqndv2lem1  37214  disjf1  46023  mapssbi  46051  supxrgere  46171  supxrgelem  46175  supxrge  46176  xrlexaddrp  46190  reclt0d  46224  uzn0bi  46295  eliccnelico  46367  qinioo  46373  iccdificc  46377  sqrlearg  46391  fsumsupp0  46416  limcrecl  46467  limsuppnflem  46546  climisp  46582  liminflbuz2  46651  climxlim2lem  46681  icccncfext  46723  stoweidlem52  46888  fourierdlem20  46963  fourierdlem34  46977  fourierdlem35  46978  fourierdlem38  46981  fourierdlem40  46983  fourierdlem41  46984  fourierdlem42  46985  fourierdlem46  46988  fourierdlem50  46992  fourierdlem60  47002  fourierdlem61  47003  fourierdlem64  47006  fourierdlem65  47007  fourierdlem72  47014  fourierdlem74  47016  fourierdlem75  47017  fourierdlem76  47018  fourierdlem78  47020  fouriersw  47067  elaa2lem  47069  etransclem24  47094  etransclem32  47102  etransclem35  47105  fge0iccico  47206  sge0cl  47217  sge0f1o  47218  sge0rernmpt  47258  meaiininclem  47322  hoidmv1lelem3  47429  hoidmvlelem2  47432  hoidmvlelem4  47434  hspmbllem2  47463  ovolval4lem1  47485  pimdecfgtioo  47553  pimincfltioo  47554  smfpimne2  47676  perfectALTVlem2  48646