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 15540 fincygsubgodd 20089 submomnd 20107 suborng 20853 perfectlem2 27193 2sqmod 27399 coltr 28715 ifnetrue 32617 nn0xmulclb 32844 ssdifidlprm 33518 1arithufdlem3 33606 1arithufdlem4 33607 ballotlemfc0 34637 ballotlemic 34651 unbdqndv2lem1 36769 disjf1 45613 mapssbi 45642 supxrgere 45763 supxrgelem 45767 supxrge 45768 xrlexaddrp 45782 reclt0d 45816 uzn0bi 45887 eliccnelico 45959 qinioo 45965 iccdificc 45969 sqrlearg 45983 fsumsupp0 46008 limcrecl 46059 limsuppnflem 46138 climisp 46174 liminflbuz2 46243 climxlim2lem 46273 icccncfext 46315 stoweidlem52 46480 fourierdlem20 46555 fourierdlem34 46569 fourierdlem35 46570 fourierdlem38 46573 fourierdlem40 46575 fourierdlem41 46576 fourierdlem42 46577 fourierdlem46 46580 fourierdlem50 46584 fourierdlem60 46594 fourierdlem61 46595 fourierdlem64 46598 fourierdlem65 46599 fourierdlem72 46606 fourierdlem74 46608 fourierdlem75 46609 fourierdlem76 46610 fourierdlem78 46612 fouriersw 46659 elaa2lem 46661 etransclem24 46686 etransclem32 46694 etransclem35 46697 fge0iccico 46798 sge0cl 46809 sge0f1o 46810 sge0rernmpt 46850 meaiininclem 46914 hoidmv1lelem3 47021 hoidmvlelem2 47024 hoidmvlelem4 47026 hspmbllem2 47055 ovolval4lem1 47077 pimdecfgtioo 47145 pimincfltioo 47146 smfpimne2 47268 perfectALTVlem2 48198