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 15485 fincygsubgodd 20027 submomnd 20045 suborng 20792 perfectlem2 27169 2sqmod 27375 coltr 28626 ifnetrue 32525 nn0xmulclb 32752 ssdifidlprm 33421 1arithufdlem3 33509 1arithufdlem4 33510 ballotlemfc0 34504 ballotlemic 34518 unbdqndv2lem1 36549 disjf1 45226 mapssbi 45256 supxrgere 45378 supxrgelem 45382 supxrge 45383 xrlexaddrp 45397 reclt0d 45431 uzn0bi 45503 eliccnelico 45575 qinioo 45581 iccdificc 45585 sqrlearg 45599 fsumsupp0 45624 limcrecl 45675 limsuppnflem 45754 climisp 45790 liminflbuz2 45859 climxlim2lem 45889 icccncfext 45931 stoweidlem52 46096 fourierdlem20 46171 fourierdlem34 46185 fourierdlem35 46186 fourierdlem38 46189 fourierdlem40 46191 fourierdlem41 46192 fourierdlem42 46193 fourierdlem46 46196 fourierdlem50 46200 fourierdlem60 46210 fourierdlem61 46211 fourierdlem64 46214 fourierdlem65 46215 fourierdlem72 46222 fourierdlem74 46224 fourierdlem75 46225 fourierdlem76 46226 fourierdlem78 46228 fouriersw 46275 elaa2lem 46277 etransclem24 46302 etransclem32 46310 etransclem35 46313 fge0iccico 46414 sge0cl 46425 sge0f1o 46426 sge0rernmpt 46466 meaiininclem 46530 hoidmv1lelem3 46637 hoidmvlelem2 46640 hoidmvlelem4 46642 hspmbllem2 46671 ovolval4lem1 46693 pimdecfgtioo 46761 pimincfltioo 46762 smfpimne2 46884 perfectALTVlem2 47759