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

Theorem pm2.65da 573
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 434 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
3 pm2.65da.2 . . 3  |-  ( (
ph  /\  ps )  ->  -.  ch )
43ex 434 . 2  |-  ( ph  ->  ( ps  ->  -.  ch ) )
52, 4pm2.65d 175 1  |-  ( ph  ->  -.  ps )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 369
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 371
This theorem is referenced by:  condan  787  nelrdva  3161  onnseq  6795  oeeulem  7032  disjen  7460  cantnflem1  7889  cantnflem1OLD  7912  ssfin4  8471  fin1a2lem12  8572  fin1a2lem13  8573  canthnumlem  8807  canthwelem  8809  supmul1  10287  ixxdisj  11307  ixxub  11313  ixxlb  11314  icodisj  11401  discr1  11988  sqrlem7  12726  bitsfzolem  13617  bitsfzo  13618  sqnprm  13771  mreexexlem2d  14570  acsinfd  15337  lbsextlem3  17167  lbsextlem4  17168  iuncon  18878  ptcmplem4  19473  iccntr  20244  evth  20377  bcthlem5  20685  ovolicopnf  20853  vitalilem4  20937  dvferm1  21303  dvferm2  21305  dgreq0  21621  radcnvle  21774  isosctrlem2  22106  mersenne  22455  pntlem3  22747  ostth2lem1  22756  tglowdim1i  22840  tgbtwndiff  22845  tgbtwnconn1lem3  22886  tglineintmo  22921  ex-natded5.5  23444  ex-natded5.8  23447  ex-natded5.13  23449  nn0min  25917  ornglmullt  26132  orngrmullt  26133  qqhre  26304  oddpwdc  26589  eulerpartlemf  26605  ballotlemfc0  26727  ballotlemfcc  26728  ballotlemimin  26740  ballotlem1c  26742  dmlogdmgm  26862  supaddc  28265  iunconlem2  31436  bnj1417  31797
  Copyright terms: Public domain W3C validator