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 15513 fincygsubgodd 20055 submomnd 20073 suborng 20821 perfectlem2 27209 2sqmod 27415 coltr 28731 ifnetrue 32633 nn0xmulclb 32861 ssdifidlprm 33550 1arithufdlem3 33638 1arithufdlem4 33639 ballotlemfc0 34670 ballotlemic 34684 unbdqndv2lem1 36728 disjf1 45539 mapssbi 45568 supxrgere 45689 supxrgelem 45693 supxrge 45694 xrlexaddrp 45708 reclt0d 45742 uzn0bi 45814 eliccnelico 45886 qinioo 45892 iccdificc 45896 sqrlearg 45910 fsumsupp0 45935 limcrecl 45986 limsuppnflem 46065 climisp 46101 liminflbuz2 46170 climxlim2lem 46200 icccncfext 46242 stoweidlem52 46407 fourierdlem20 46482 fourierdlem34 46496 fourierdlem35 46497 fourierdlem38 46500 fourierdlem40 46502 fourierdlem41 46503 fourierdlem42 46504 fourierdlem46 46507 fourierdlem50 46511 fourierdlem60 46521 fourierdlem61 46522 fourierdlem64 46525 fourierdlem65 46526 fourierdlem72 46533 fourierdlem74 46535 fourierdlem75 46536 fourierdlem76 46537 fourierdlem78 46539 fouriersw 46586 elaa2lem 46588 etransclem24 46613 etransclem32 46621 etransclem35 46624 fge0iccico 46725 sge0cl 46736 sge0f1o 46737 sge0rernmpt 46777 meaiininclem 46841 hoidmv1lelem3 46948 hoidmvlelem2 46951 hoidmvlelem4 46953 hspmbllem2 46982 ovolval4lem1 47004 pimdecfgtioo 47072 pimincfltioo 47073 smfpimne2 47195 perfectALTVlem2 48079