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 823

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 822	. 2 ⊢ (𝜑 → ¬ ¬ 𝜓)
4	3	notnotrd 133	1 ⊢ (𝜑 → 𝜓)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 396

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 208 df-an 397

This theorem is referenced by: rlimcld2 15538 fincygsubgodd 20087 submomnd 20105 suborng 20855 perfectlem2 27218 2sqmod 27424 coltr 28740 ifnetrue 32642 nn0xmulclb 32870 ssdifidlprm 33548 1arithufdlem3 33636 1arithufdlem4 33637 ballotlemfc0 34684 ballotlemic 34698 unbdqndv2lem1 36822 disjf1 45637 mapssbi 45665 supxrgere 45785 supxrgelem 45789 supxrge 45790 xrlexaddrp 45804 reclt0d 45838 uzn0bi 45909 eliccnelico 45981 qinioo 45987 iccdificc 45991 sqrlearg 46005 fsumsupp0 46030 limcrecl 46081 limsuppnflem 46160 climisp 46196 liminflbuz2 46265 climxlim2lem 46295 icccncfext 46337 stoweidlem52 46502 fourierdlem20 46577 fourierdlem34 46591 fourierdlem35 46592 fourierdlem38 46595 fourierdlem40 46597 fourierdlem41 46598 fourierdlem42 46599 fourierdlem46 46602 fourierdlem50 46606 fourierdlem60 46616 fourierdlem61 46617 fourierdlem64 46620 fourierdlem65 46621 fourierdlem72 46628 fourierdlem74 46630 fourierdlem75 46631 fourierdlem76 46632 fourierdlem78 46634 fouriersw 46681 elaa2lem 46683 etransclem24 46708 etransclem32 46716 etransclem35 46719 fge0iccico 46820 sge0cl 46831 sge0f1o 46832 sge0rernmpt 46872 meaiininclem 46936 hoidmv1lelem3 47043 hoidmvlelem2 47046 hoidmvlelem4 47048 hspmbllem2 47077 ovolval4lem1 47099 pimdecfgtioo 47167 pimincfltioo 47168 smfpimne2 47290 perfectALTVlem2 48220