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  15750  fincygsubgodd  20333  submomnd  20351  suborng  21138  ssdifidlprm  21647  perfectlem2  27562  2sqmod  27768  coltr  29121  prlngmo2  29439  ifnetrue  33190  nn0xmulclb  33409  dflringlem  34072  dflring3  34075  dflring4  34076  1arithufdlem3  34124  1arithufdlem4  34125  ballotlemfc0  35171  ballotlemic  35185  unbdqndv2lem1  37467  disjf1  46291  mapssbi  46319  supxrgere  46438  supxrgelem  46442  supxrge  46443  xrlexaddrp  46457  reclt0d  46491  uzn0bi  46562  eliccnelico  46634  qinioo  46640  iccdificc  46644  sqrlearg  46658  fsumsupp0  46683  limcrecl  46734  limsuppnflem  46813  climisp  46849  liminflbuz2  46918  climxlim2lem  46948  icccncfext  46990  stoweidlem52  47155  fourierdlem20  47230  fourierdlem34  47244  fourierdlem35  47245  fourierdlem38  47248  fourierdlem40  47250  fourierdlem41  47251  fourierdlem42  47252  fourierdlem46  47255  fourierdlem50  47259  fourierdlem60  47269  fourierdlem61  47270  fourierdlem64  47273  fourierdlem65  47274  fourierdlem72  47281  fourierdlem74  47283  fourierdlem75  47284  fourierdlem76  47285  fourierdlem78  47287  fouriersw  47334  elaa2lem  47336  etransclem24  47361  etransclem32  47369  etransclem35  47372  fge0iccico  47473  sge0cl  47484  sge0f1o  47485  sge0rernmpt  47525  meaiininclem  47589  hoidmv1lelem3  47696  hoidmvlelem2  47699  hoidmvlelem4  47701  hspmbllem2  47730  ovolval4lem1  47752  pimdecfgtioo  47820  pimincfltioo  47821  smfpimne2  47943  perfectALTVlem2  48913  parhomeqor2  50851  parhomeqor  50852