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 15544 fincygsubgodd 20044 perfectlem2 27141 2sqmod 27347 coltr 28574 ifnetrue 32476 nn0xmulclb 32694 submomnd 33024 suborng 33293 ssdifidlprm 33429 1arithufdlem3 33517 1arithufdlem4 33518 ballotlemfc0 34484 ballotlemic 34498 unbdqndv2lem1 36497 disjf1 45177 mapssbi 45207 supxrgere 45329 supxrgelem 45333 supxrge 45334 xrlexaddrp 45348 reclt0d 45383 uzn0bi 45455 eliccnelico 45527 qinioo 45533 iccdificc 45537 sqrlearg 45551 fsumsupp0 45576 limcrecl 45627 limsuppnflem 45708 climisp 45744 liminflbuz2 45813 climxlim2lem 45843 icccncfext 45885 stoweidlem52 46050 fourierdlem20 46125 fourierdlem34 46139 fourierdlem35 46140 fourierdlem38 46143 fourierdlem40 46145 fourierdlem41 46146 fourierdlem42 46147 fourierdlem46 46150 fourierdlem50 46154 fourierdlem60 46164 fourierdlem61 46165 fourierdlem64 46168 fourierdlem65 46169 fourierdlem72 46176 fourierdlem74 46178 fourierdlem75 46179 fourierdlem76 46180 fourierdlem78 46182 fouriersw 46229 elaa2lem 46231 etransclem24 46256 etransclem32 46264 etransclem35 46267 fge0iccico 46368 sge0cl 46379 sge0f1o 46380 sge0rernmpt 46420 meaiininclem 46484 hoidmv1lelem3 46591 hoidmvlelem2 46594 hoidmvlelem4 46596 hspmbllem2 46625 ovolval4lem1 46647 pimdecfgtioo 46715 pimincfltioo 46716 smfpimne2 46838 perfectALTVlem2 47723