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

Theorem pm2.65da 576
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  792  nelrdva  3168  onnseq  6805  oeeulem  7040  disjen  7468  cantnflem1  7897  cantnflem1OLD  7920  ssfin4  8479  fin1a2lem12  8580  fin1a2lem13  8581  canthnumlem  8815  canthwelem  8817  supmul1  10295  ixxdisj  11315  ixxub  11321  ixxlb  11322  icodisj  11410  discr1  12000  sqrlem7  12738  bitsfzolem  13630  bitsfzo  13631  sqnprm  13784  mreexexlem2d  14583  acsinfd  15350  lbsextlem3  17241  lbsextlem4  17242  iuncon  19032  ptcmplem4  19627  iccntr  20398  evth  20531  bcthlem5  20839  ovolicopnf  21007  vitalilem4  21091  dvferm1  21457  dvferm2  21459  dgreq0  21732  radcnvle  21885  isosctrlem2  22217  mersenne  22566  pntlem3  22858  ostth2lem1  22867  tglowdim1i  22954  tgbtwndiff  22959  tgbtwnconn1lem3  23006  tglineintmo  23047  tglineneq  23049  krippenlem  23084  midexlem  23086  ragncol  23102  footex  23109  ex-natded5.5  23617  ex-natded5.8  23620  ex-natded5.13  23622  nn0min  26090  ornglmullt  26275  orngrmullt  26276  qqhre  26446  oddpwdc  26737  eulerpartlemf  26753  ballotlemfc0  26875  ballotlemfcc  26876  ballotlemimin  26888  ballotlem1c  26890  dmlogdmgm  27010  supaddc  28417  iunconlem2  31671  bnj1417  32032
  Copyright terms: Public domain W3C validator