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 818

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 817	. 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 15614 fincygsubgodd 20132 perfectlem2 27274 2sqmod 27480 coltr 28655 ifnetrue 32560 nn0xmulclb 32775 submomnd 33087 suborng 33345 ssdifidlprm 33486 1arithufdlem3 33574 1arithufdlem4 33575 ballotlemfc0 34495 ballotlemic 34509 unbdqndv2lem1 36510 disjf1 45188 mapssbi 45218 supxrgere 45344 supxrgelem 45348 supxrge 45349 xrlexaddrp 45363 reclt0d 45398 uzn0bi 45470 eliccnelico 45542 qinioo 45548 iccdificc 45552 sqrlearg 45566 fsumsupp0 45593 limcrecl 45644 limsuppnflem 45725 climisp 45761 liminflbuz2 45830 climxlim2lem 45860 icccncfext 45902 stoweidlem52 46067 fourierdlem20 46142 fourierdlem34 46156 fourierdlem35 46157 fourierdlem38 46160 fourierdlem40 46162 fourierdlem41 46163 fourierdlem42 46164 fourierdlem46 46167 fourierdlem50 46171 fourierdlem60 46181 fourierdlem61 46182 fourierdlem64 46185 fourierdlem65 46186 fourierdlem72 46193 fourierdlem74 46195 fourierdlem75 46196 fourierdlem76 46197 fourierdlem78 46199 fouriersw 46246 elaa2lem 46248 etransclem24 46273 etransclem32 46281 etransclem35 46284 fge0iccico 46385 sge0cl 46396 sge0f1o 46397 sge0rernmpt 46437 meaiininclem 46501 hoidmv1lelem3 46608 hoidmvlelem2 46611 hoidmvlelem4 46613 hspmbllem2 46642 ovolval4lem1 46664 pimdecfgtioo 46732 pimincfltioo 46733 smfpimne2 46855 perfectALTVlem2 47709