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 15610 fincygsubgodd 20146 perfectlem2 27288 2sqmod 27494 coltr 28669 ifnetrue 32567 nn0xmulclb 32781 submomnd 33069 suborng 33324 ssdifidlprm 33465 1arithufdlem3 33553 1arithufdlem4 33554 ballotlemfc0 34473 ballotlemic 34487 unbdqndv2lem1 36491 disjf1 45125 mapssbi 45155 supxrgere 45282 supxrgelem 45286 supxrge 45287 xrlexaddrp 45301 reclt0d 45336 uzn0bi 45408 eliccnelico 45481 qinioo 45487 iccdificc 45491 sqrlearg 45505 fsumsupp0 45533 limcrecl 45584 limsuppnflem 45665 climisp 45701 liminflbuz2 45770 climxlim2lem 45800 icccncfext 45842 stoweidlem52 46007 fourierdlem20 46082 fourierdlem34 46096 fourierdlem35 46097 fourierdlem38 46100 fourierdlem40 46102 fourierdlem41 46103 fourierdlem42 46104 fourierdlem46 46107 fourierdlem50 46111 fourierdlem60 46121 fourierdlem61 46122 fourierdlem64 46125 fourierdlem65 46126 fourierdlem72 46133 fourierdlem74 46135 fourierdlem75 46136 fourierdlem76 46137 fourierdlem78 46139 fouriersw 46186 elaa2lem 46188 etransclem24 46213 etransclem32 46221 etransclem35 46224 fge0iccico 46325 sge0cl 46336 sge0f1o 46337 sge0rernmpt 46377 meaiininclem 46441 hoidmv1lelem3 46548 hoidmvlelem2 46551 hoidmvlelem4 46553 hspmbllem2 46582 ovolval4lem1 46604 pimdecfgtioo 46672 pimincfltioo 46673 smfpimne2 46795 perfectALTVlem2 47646