MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm2.65da Unicode version

Theorem pm2.65da 559
Description: Deduction rule for proof by contradiction. (Contributed by NM, 12-Jun-2014.)
Hypotheses
Ref Expression
pm2.65da.1  |-  ( (
ph  /\  ps )  ->  ch )
pm2.65da.2  |-  ( (
ph  /\  ps )  ->  -.  ch )
Assertion
Ref Expression
pm2.65da  |-  ( ph  ->  -.  ps )

Proof of Theorem pm2.65da
StepHypRef Expression
1 pm2.65da.1 . . 3  |-  ( (
ph  /\  ps )  ->  ch )
21ex 423 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
3 pm2.65da.2 . . 3  |-  ( (
ph  /\  ps )  ->  -.  ch )
43ex 423 . 2  |-  ( ph  ->  ( ps  ->  -.  ch ) )
52, 4pm2.65d 166 1  |-  ( ph  ->  -.  ps )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 358
This theorem is referenced by:  condan  769  onnseq  6377  oeeulem  6615  disjen  7034  cantnflem1  7407  ssfin4  7952  fin1a2lem12  8053  fin1a2lem13  8054  canthnumlem  8286  canthwelem  8288  supmul1  9735  ixxdisj  10687  ixxub  10693  ixxlb  10694  icodisj  10777  discr1  11253  sqrlem7  11750  bitsfzolem  12641  bitsfzo  12642  sqnprm  12793  ramlb  13082  mreexexlem2d  13563  acsinfd  14299  lbsextlem3  15929  lbsextlem4  15930  iuncon  17170  ptcmplem4  17765  iccntr  18342  evth  18473  bcthlem5  18766  ovolicopnf  18899  vitalilem4  18982  dvferm1  19348  dvferm2  19350  dgreq0  19662  radcnvle  19812  isosctrlem2  20135  mersenne  20482  pntlem3  20774  ostth2lem1  20783  ex-natded5.5  20813  ex-natded5.8  20816  ex-natded5.13  20818  ballotlemfc0  23067  ballotlemfcc  23068  ballotlemimin  23080  ballotlem1c  23082  supaddc  24995  bnj1417  29387
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator