Theorem condan 816

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

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

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 209  df-an 399

This theorem is referenced by:  rlimcld2  14935  fincygsubgodd  19234  perfectlem2  25806  2sqmod  26012  coltr  26433  nn0xmulclb  30496  submomnd  30711  suborng  30888  ballotlemfc0  31750  ballotlemic  31764  unbdqndv2lem1  33848  disjf1  41492  mapssbi  41525  supxrgere  41650  supxrgelem  41654  supxrge  41655  xrlexaddrp  41669  reclt0d  41707  uzn0bi  41784  eliccnelico  41854  qinioo  41860  iccdificc  41864  sqrlearg  41878  fsumsupp0  41908  limcrecl  41959  limsuppnflem  42040  climisp  42076  liminflbuz2  42145  climxlim2lem  42175  icccncfext  42219  stoweidlem52  42386  fourierdlem20  42461  fourierdlem34  42475  fourierdlem35  42476  fourierdlem38  42479  fourierdlem40  42481  fourierdlem41  42482  fourierdlem42  42483  fourierdlem46  42486  fourierdlem50  42490  fourierdlem60  42500  fourierdlem61  42501  fourierdlem64  42504  fourierdlem65  42505  fourierdlem72  42512  fourierdlem74  42514  fourierdlem75  42515  fourierdlem76  42516  fourierdlem78  42518  fouriersw  42565  elaa2lem  42567  etransclem24  42592  etransclem32  42600  etransclem35  42603  fge0iccico  42701  sge0cl  42712  sge0f1o  42713  sge0rernmpt  42753  meaiininclem  42817  hoidmv1lelem3  42924  hoidmvlelem2  42927  hoidmvlelem4  42929  hspmbllem2  42958  ovolval4lem1  42980  pimdecfgtioo  43044  pimincfltioo  43045  perfectALTVlem2  43936