condan - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > condan		Structured version Visualization version GIF version

Theorem condan 817

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

Colors of variables: wff setvar class

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

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 207 df-an 396

This theorem is referenced by: rlimcld2 15551 fincygsubgodd 20051 perfectlem2 27148 2sqmod 27354 coltr 28581 ifnetrue 32483 nn0xmulclb 32701 submomnd 33031 suborng 33300 ssdifidlprm 33436 1arithufdlem3 33524 1arithufdlem4 33525 ballotlemfc0 34491 ballotlemic 34505 unbdqndv2lem1 36504 disjf1 45184 mapssbi 45214 supxrgere 45336 supxrgelem 45340 supxrge 45341 xrlexaddrp 45355 reclt0d 45390 uzn0bi 45462 eliccnelico 45534 qinioo 45540 iccdificc 45544 sqrlearg 45558 fsumsupp0 45583 limcrecl 45634 limsuppnflem 45715 climisp 45751 liminflbuz2 45820 climxlim2lem 45850 icccncfext 45892 stoweidlem52 46057 fourierdlem20 46132 fourierdlem34 46146 fourierdlem35 46147 fourierdlem38 46150 fourierdlem40 46152 fourierdlem41 46153 fourierdlem42 46154 fourierdlem46 46157 fourierdlem50 46161 fourierdlem60 46171 fourierdlem61 46172 fourierdlem64 46175 fourierdlem65 46176 fourierdlem72 46183 fourierdlem74 46185 fourierdlem75 46186 fourierdlem76 46187 fourierdlem78 46189 fouriersw 46236 elaa2lem 46238 etransclem24 46263 etransclem32 46271 etransclem35 46274 fge0iccico 46375 sge0cl 46386 sge0f1o 46387 sge0rernmpt 46427 meaiininclem 46491 hoidmv1lelem3 46598 hoidmvlelem2 46601 hoidmvlelem4 46603 hspmbllem2 46632 ovolval4lem1 46654 pimdecfgtioo 46722 pimincfltioo 46723 smfpimne2 46845 perfectALTVlem2 47727