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

Theorem condan 811
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 586 . 2  |-  ( ph  ->  -.  -.  ps )
43notnotrd 117 1  |-  ( ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 376
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 190  df-an 378
This theorem is referenced by:  rlimcld2  13719  perfectlem2  24237  coltr  24771  2sqmod  28484  submomnd  28547  suborng  28652  ballotlemfc0  29398  ballotlemic  29412  ballotlemicOLD  29450  disjf1  37528  mapssbi  37566  supxrgere  37643  supxrgelem  37647  supxrge  37648  xrlexaddrp  37662  eliccnelico  37727  qinioo  37733  iccdificc  37737  fsumsupp0  37753  limcrecl  37806  icccncfext  37862  stoweidlem52  38025  fourierdlem20  38101  fourierdlem34  38116  fourierdlem35  38117  fourierdlem38  38120  fourierdlem40  38122  fourierdlem41  38123  fourierdlem42  38124  fourierdlem42OLD  38125  fourierdlem46  38128  fourierdlem50  38132  fourierdlem60  38142  fourierdlem61  38143  fourierdlem64  38146  fourierdlem65  38147  fourierdlem72  38154  fourierdlem74  38156  fourierdlem75  38157  fourierdlem76  38158  fourierdlem78  38160  fouriersw  38207  elaa2lem  38209  elaa2lemOLD  38210  etransclem24  38235  etransclem32  38243  etransclem35  38246  fge0iccico  38326  sge0cl  38337  sge0f1o  38338  sge0rernmpt  38378  hoidmv1lelem3  38533  hoidmvlelem2  38536  hoidmvlelem4  38538  hspmbllem2  38567  ovolval4lem1  38589  perfectALTVlem2  38989
  Copyright terms: Public domain W3C validator