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 15624 fincygsubgodd 20156 perfectlem2 27292 2sqmod 27498 coltr 28673 ifnetrue 32570 nn0xmulclb 32778 submomnd 33060 suborng 33310 ssdifidlprm 33451 1arithufdlem3 33539 1arithufdlem4 33540 ballotlemfc0 34457 ballotlemic 34471 unbdqndv2lem1 36475 disjf1 45090 mapssbi 45120 supxrgere 45248 supxrgelem 45252 supxrge 45253 xrlexaddrp 45267 reclt0d 45302 uzn0bi 45374 eliccnelico 45447 qinioo 45453 iccdificc 45457 sqrlearg 45471 fsumsupp0 45499 limcrecl 45550 limsuppnflem 45631 climisp 45667 liminflbuz2 45736 climxlim2lem 45766 icccncfext 45808 stoweidlem52 45973 fourierdlem20 46048 fourierdlem34 46062 fourierdlem35 46063 fourierdlem38 46066 fourierdlem40 46068 fourierdlem41 46069 fourierdlem42 46070 fourierdlem46 46073 fourierdlem50 46077 fourierdlem60 46087 fourierdlem61 46088 fourierdlem64 46091 fourierdlem65 46092 fourierdlem72 46099 fourierdlem74 46101 fourierdlem75 46102 fourierdlem76 46103 fourierdlem78 46105 fouriersw 46152 elaa2lem 46154 etransclem24 46179 etransclem32 46187 etransclem35 46190 fge0iccico 46291 sge0cl 46302 sge0f1o 46303 sge0rernmpt 46343 meaiininclem 46407 hoidmv1lelem3 46514 hoidmvlelem2 46517 hoidmvlelem4 46519 hspmbllem2 46548 ovolval4lem1 46570 pimdecfgtioo 46638 pimincfltioo 46639 smfpimne2 46761 perfectALTVlem2 47596