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 15487 fincygsubgodd 20028 submomnd 20046 suborng 20793 perfectlem2 27169 2sqmod 27375 coltr 28626 ifnetrue 32529 nn0xmulclb 32758 ssdifidlprm 33430 1arithufdlem3 33518 1arithufdlem4 33519 ballotlemfc0 34527 ballotlemic 34541 unbdqndv2lem1 36574 disjf1 45305 mapssbi 45335 supxrgere 45457 supxrgelem 45461 supxrge 45462 xrlexaddrp 45476 reclt0d 45510 uzn0bi 45582 eliccnelico 45654 qinioo 45660 iccdificc 45664 sqrlearg 45678 fsumsupp0 45703 limcrecl 45754 limsuppnflem 45833 climisp 45869 liminflbuz2 45938 climxlim2lem 45968 icccncfext 46010 stoweidlem52 46175 fourierdlem20 46250 fourierdlem34 46264 fourierdlem35 46265 fourierdlem38 46268 fourierdlem40 46270 fourierdlem41 46271 fourierdlem42 46272 fourierdlem46 46275 fourierdlem50 46279 fourierdlem60 46289 fourierdlem61 46290 fourierdlem64 46293 fourierdlem65 46294 fourierdlem72 46301 fourierdlem74 46303 fourierdlem75 46304 fourierdlem76 46305 fourierdlem78 46307 fouriersw 46354 elaa2lem 46356 etransclem24 46381 etransclem32 46389 etransclem35 46392 fge0iccico 46493 sge0cl 46504 sge0f1o 46505 sge0rernmpt 46545 meaiininclem 46609 hoidmv1lelem3 46716 hoidmvlelem2 46719 hoidmvlelem4 46721 hspmbllem2 46750 ovolval4lem1 46772 pimdecfgtioo 46840 pimincfltioo 46841 smfpimne2 46963 perfectALTVlem2 47847