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 15594 fincygsubgodd 20095 perfectlem2 27193 2sqmod 27399 coltr 28626 ifnetrue 32528 nn0xmulclb 32748 submomnd 33078 suborng 33337 ssdifidlprm 33473 1arithufdlem3 33561 1arithufdlem4 33562 ballotlemfc0 34525 ballotlemic 34539 unbdqndv2lem1 36527 disjf1 45207 mapssbi 45237 supxrgere 45360 supxrgelem 45364 supxrge 45365 xrlexaddrp 45379 reclt0d 45414 uzn0bi 45486 eliccnelico 45558 qinioo 45564 iccdificc 45568 sqrlearg 45582 fsumsupp0 45607 limcrecl 45658 limsuppnflem 45739 climisp 45775 liminflbuz2 45844 climxlim2lem 45874 icccncfext 45916 stoweidlem52 46081 fourierdlem20 46156 fourierdlem34 46170 fourierdlem35 46171 fourierdlem38 46174 fourierdlem40 46176 fourierdlem41 46177 fourierdlem42 46178 fourierdlem46 46181 fourierdlem50 46185 fourierdlem60 46195 fourierdlem61 46196 fourierdlem64 46199 fourierdlem65 46200 fourierdlem72 46207 fourierdlem74 46209 fourierdlem75 46210 fourierdlem76 46211 fourierdlem78 46213 fouriersw 46260 elaa2lem 46262 etransclem24 46287 etransclem32 46295 etransclem35 46298 fge0iccico 46399 sge0cl 46410 sge0f1o 46411 sge0rernmpt 46451 meaiininclem 46515 hoidmv1lelem3 46622 hoidmvlelem2 46625 hoidmvlelem4 46627 hspmbllem2 46656 ovolval4lem1 46678 pimdecfgtioo 46746 pimincfltioo 46747 smfpimne2 46869 perfectALTVlem2 47736