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  6361  oeeulem  6599  disjen  7018  cantnflem1  7391  ssfin4  7936  fin1a2lem12  8037  fin1a2lem13  8038  canthnumlem  8270  canthwelem  8272  supmul1  9719  ixxdisj  10671  ixxub  10677  ixxlb  10678  icodisj  10761  discr1  11237  sqrlem7  11734  bitsfzolem  12625  bitsfzo  12626  sqnprm  12777  ramlb  13066  mreexexlem2d  13547  acsinfd  14283  lbsextlem3  15913  lbsextlem4  15914  iuncon  17154  ptcmplem4  17749  iccntr  18326  evth  18457  bcthlem5  18750  ovolicopnf  18883  vitalilem4  18966  dvferm1  19332  dvferm2  19334  dgreq0  19646  radcnvle  19796  isosctrlem2  20119  mersenne  20466  pntlem3  20758  ostth2lem1  20767  ex-natded5.5  20797  ex-natded5.8  20800  ex-natded5.13  20802  ballotlemfc0  23051  ballotlemfcc  23052  ballotlemimin  23064  ballotlem1c  23066  bnj1417  29071
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