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

Theorem condan 792
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 574 . 2  |-  ( ph  ->  -.  -.  ps )
43notnotrd 113 1  |-  ( ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 367
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 185  df-an 369
This theorem is referenced by:  rlimcld2  13483  perfectlem2  23703  coltr  24228  coltr2  24229  2sqmod  27870  submomnd  27934  suborng  28040  ballotlemfc0  28695  ballotlemic  28709  limcrecl  31874  icccncfext  31929  stoweidlem52  32073  fourierdlem20  32148  fourierdlem34  32162  fourierdlem35  32163  fourierdlem38  32166  fourierdlem40  32168  fourierdlem41  32169  fourierdlem42  32170  fourierdlem46  32174  fourierdlem50  32178  fourierdlem60  32188  fourierdlem61  32189  fourierdlem64  32192  fourierdlem65  32193  fourierdlem72  32200  fourierdlem74  32202  fourierdlem75  32203  fourierdlem76  32204  fourierdlem78  32206  fouriersw  32253  elaa2lem  32255  etransclem24  32280  etransclem32  32288  etransclem35  32291
  Copyright terms: Public domain W3C validator