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 15531 fincygsubgodd 20080 submomnd 20098 suborng 20844 perfectlem2 27207 2sqmod 27413 coltr 28729 ifnetrue 32632 nn0xmulclb 32859 ssdifidlprm 33533 1arithufdlem3 33621 1arithufdlem4 33622 ballotlemfc0 34653 ballotlemic 34667 unbdqndv2lem1 36785 disjf1 45631 mapssbi 45660 supxrgere 45781 supxrgelem 45785 supxrge 45786 xrlexaddrp 45800 reclt0d 45834 uzn0bi 45905 eliccnelico 45977 qinioo 45983 iccdificc 45987 sqrlearg 46001 fsumsupp0 46026 limcrecl 46077 limsuppnflem 46156 climisp 46192 liminflbuz2 46261 climxlim2lem 46291 icccncfext 46333 stoweidlem52 46498 fourierdlem20 46573 fourierdlem34 46587 fourierdlem35 46588 fourierdlem38 46591 fourierdlem40 46593 fourierdlem41 46594 fourierdlem42 46595 fourierdlem46 46598 fourierdlem50 46602 fourierdlem60 46612 fourierdlem61 46613 fourierdlem64 46616 fourierdlem65 46617 fourierdlem72 46624 fourierdlem74 46626 fourierdlem75 46627 fourierdlem76 46628 fourierdlem78 46630 fouriersw 46677 elaa2lem 46679 etransclem24 46704 etransclem32 46712 etransclem35 46715 fge0iccico 46816 sge0cl 46827 sge0f1o 46828 sge0rernmpt 46868 meaiininclem 46932 hoidmv1lelem3 47039 hoidmvlelem2 47042 hoidmvlelem4 47044 hspmbllem2 47073 ovolval4lem1 47095 pimdecfgtioo 47163 pimincfltioo 47164 smfpimne2 47286 perfectALTVlem2 48210