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 15501 fincygsubgodd 20043 submomnd 20061 suborng 20809 perfectlem2 27197 2sqmod 27403 coltr 28719 ifnetrue 32622 nn0xmulclb 32851 ssdifidlprm 33539 1arithufdlem3 33627 1arithufdlem4 33628 ballotlemfc0 34650 ballotlemic 34664 unbdqndv2lem1 36709 disjf1 45427 mapssbi 45457 supxrgere 45578 supxrgelem 45582 supxrge 45583 xrlexaddrp 45597 reclt0d 45631 uzn0bi 45703 eliccnelico 45775 qinioo 45781 iccdificc 45785 sqrlearg 45799 fsumsupp0 45824 limcrecl 45875 limsuppnflem 45954 climisp 45990 liminflbuz2 46059 climxlim2lem 46089 icccncfext 46131 stoweidlem52 46296 fourierdlem20 46371 fourierdlem34 46385 fourierdlem35 46386 fourierdlem38 46389 fourierdlem40 46391 fourierdlem41 46392 fourierdlem42 46393 fourierdlem46 46396 fourierdlem50 46400 fourierdlem60 46410 fourierdlem61 46411 fourierdlem64 46414 fourierdlem65 46415 fourierdlem72 46422 fourierdlem74 46424 fourierdlem75 46425 fourierdlem76 46426 fourierdlem78 46428 fouriersw 46475 elaa2lem 46477 etransclem24 46502 etransclem32 46510 etransclem35 46513 fge0iccico 46614 sge0cl 46625 sge0f1o 46626 sge0rernmpt 46666 meaiininclem 46730 hoidmv1lelem3 46837 hoidmvlelem2 46840 hoidmvlelem4 46842 hspmbllem2 46871 ovolval4lem1 46893 pimdecfgtioo 46961 pimincfltioo 46962 smfpimne2 47084 perfectALTVlem2 47968