MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  condan Structured version   Unicode version

Theorem condan 801
Description: Proof by contradiction. (Contributed by NM, 9-Feb-2006.) (Proof shortened by Wolf Lammen, 19-Jun-2014.)
Hypotheses
Ref Expression
condan.1  |-  ( (
ph  /\  -.  ps )  ->  ch )
condan.2  |-  ( (
ph  /\  -.  ps )  ->  -.  ch )
Assertion
Ref Expression
condan  |-  ( ph  ->  ps )

Proof of Theorem condan
StepHypRef Expression
1 condan.1 . . 3  |-  ( (
ph  /\  -.  ps )  ->  ch )
2 condan.2 . . 3  |-  ( (
ph  /\  -.  ps )  ->  -.  ch )
31, 2pm2.65da 578 . 2  |-  ( ph  ->  -.  -.  ps )
43notnotrd 116 1  |-  ( ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 370
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 188  df-an 372
This theorem is referenced by:  rlimcld2  13620  perfectlem2  24021  coltr  24551  coltr2  24552  2sqmod  28247  submomnd  28311  suborng  28417  ballotlemfc0  29151  ballotlemic  29165  disjf1  37080  supxrgere  37165  supxrgelem  37169  supxrge  37170  eliccnelico  37216  limcrecl  37281  icccncfext  37337  stoweidlem52  37482  fourierdlem20  37558  fourierdlem34  37572  fourierdlem35  37573  fourierdlem38  37576  fourierdlem40  37578  fourierdlem41  37579  fourierdlem42  37580  fourierdlem46  37584  fourierdlem50  37588  fourierdlem60  37598  fourierdlem61  37599  fourierdlem64  37602  fourierdlem65  37603  fourierdlem72  37610  fourierdlem74  37612  fourierdlem75  37613  fourierdlem76  37614  fourierdlem78  37616  fouriersw  37663  elaa2lem  37665  etransclem24  37690  etransclem32  37698  etransclem35  37701  fge0iccico  37746  sge0cl  37757  sge0f1o  37758  perfectALTVlem2  38243
  Copyright terms: Public domain W3C validator