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 15503 fincygsubgodd 20011 submomnd 20029 suborng 20779 perfectlem2 27157 2sqmod 27363 coltr 28610 ifnetrue 32509 nn0xmulclb 32727 ssdifidlprm 33408 1arithufdlem3 33496 1arithufdlem4 33497 ballotlemfc0 34463 ballotlemic 34477 unbdqndv2lem1 36485 disjf1 45164 mapssbi 45194 supxrgere 45316 supxrgelem 45320 supxrge 45321 xrlexaddrp 45335 reclt0d 45370 uzn0bi 45442 eliccnelico 45514 qinioo 45520 iccdificc 45524 sqrlearg 45538 fsumsupp0 45563 limcrecl 45614 limsuppnflem 45695 climisp 45731 liminflbuz2 45800 climxlim2lem 45830 icccncfext 45872 stoweidlem52 46037 fourierdlem20 46112 fourierdlem34 46126 fourierdlem35 46127 fourierdlem38 46130 fourierdlem40 46132 fourierdlem41 46133 fourierdlem42 46134 fourierdlem46 46137 fourierdlem50 46141 fourierdlem60 46151 fourierdlem61 46152 fourierdlem64 46155 fourierdlem65 46156 fourierdlem72 46163 fourierdlem74 46165 fourierdlem75 46166 fourierdlem76 46167 fourierdlem78 46169 fouriersw 46216 elaa2lem 46218 etransclem24 46243 etransclem32 46251 etransclem35 46254 fge0iccico 46355 sge0cl 46366 sge0f1o 46367 sge0rernmpt 46407 meaiininclem 46471 hoidmv1lelem3 46578 hoidmvlelem2 46581 hoidmvlelem4 46583 hspmbllem2 46612 ovolval4lem1 46634 pimdecfgtioo 46702 pimincfltioo 46703 smfpimne2 46825 perfectALTVlem2 47710