Theorem pm2.65da 578

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

Step	Hyp	Ref	Expression
1		pm2.65da.1	. . 3 |- ( ( ph /\ ps ) -> ch )
2	1	ex 435	. 2 |- ( ph -> ( ps -> ch ) )
3		pm2.65da.2	. . 3 |- ( ( ph /\ ps ) -> -. ch )
4	3	ex 435	. 2 |- ( ph -> ( ps -> -. ch ) )
5	2, 4	pm2.65d 178	1 |- ( ph -> -. ps )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 370

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 188  df-an 372

This theorem is referenced by:  condan  801  nelrdva  3281  onnseq  7074  oeeulem  7313  disjen  7738  cantnflem1  8202  ssfin4  8747  fin1a2lem12  8848  fin1a2lem13  8849  canthnumlem  9080  canthwelem  9082  supaddc  10581  supmul1  10583  ixxdisj  11657  ixxub  11663  ixxlb  11664  ixxlbOLD  11665  icodisj  11764  discr1  12414  sqrlem7  13312  bitsfzolem  14406  bitsfzolemOLD  14407  bitsfzo  14408  sqnprm  14645  mreexexlem2d  15550  acsinfd  16425  lbsextlem3  18382  lbsextlem4  18383  iuncon  20441  dissnlocfin  20542  ptcmplem4  21068  iccntr  21837  evth  21985  bcthlem5  22294  ovolicopnf  22476  vitalilem4  22567  dvferm1  22935  dvferm2  22937  dgreq0  23217  radcnvle  23373  isosctrlem2  23746  dmlogdmgm  23947  mersenne  24153  pntlem3  24445  ostth2lem1  24454  tgbtwnne  24532  tglowdim1i  24543  tgbtwndiff  24548  tgbtwnconn1lem3  24617  legso  24642  tglineintmo  24685  tglineneq  24687  tglowdim2ln  24694  mirne  24710  mirhl  24722  krippenlem  24733  midexlem  24735  footex  24761  colperpexlem3  24772  mideulem2  24774  opphllem  24775  oppne3  24783  oppnid  24786  opphllem1  24787  opphllem2  24788  outpasch  24795  hlpasch  24796  hpgerlem  24805  colhp  24810  trgcopy  24844  cgrancol  24868  tgasa1  24887  ex-natded5.5  25858  ex-natded5.8  25861  ex-natded5.13  25863  nn0min  28391  2sqn0  28414  ornglmullt  28578  orngrmullt  28579  qqhre  28832  esumcvgre  28920  carsgclctunlem2  29159  oddpwdc  29195  eulerpartlemf  29211  ballotlemfc0  29333  ballotlemfcc  29334  ballotlemimin  29346  ballotlem1c  29348  ballotlemiminOLD  29384  ballotlem1cOLD  29386  bnj1417  29858  topdifinffinlem  31714  poimirlem11  31915  poimirlem12  31916  imo72b2  36589  iunconlem2  37305  n0p  37349  uzwo4  37365  disjrnmpt2  37424  xrlexaddrp  37529  icoub  37576  limclner  37672  icccncfext  37705  fperdvper  37730  dvdivbd  37735  dvdsn1add  37754  dvmptfprodlem  37759  dvnprodlem3  37763  fourierdlem10  37919  fourierdlem19  37928  fourierdlem20  37929  fourierdlem35  37945  fourierdlem40  37950  fourierdlem41  37951  fourierdlem42  37952  fourierdlem42OLD  37953  fourierdlem46  37956  fourierdlem48  37958  fourierdlem49  37959  fourierdlem57  37967  fourierdlem58  37968  fourierdlem59  37969  fourierdlem63  37973  fourierdlem64  37974  fourierdlem65  37975  fourierdlem68  37978  fourierdlem74  37984  fourierdlem75  37985  fourierdlem78  37988  fourierdlem79  37989  fourierdlem80  37990  elaa2  38039  etransclem35  38074  etransclem38  38077  prsal  38100  fge0npnf  38117  sge0tsms  38130  sge0rern  38138  sge0supre  38139  sge0le  38157  sge0fodjrnlem  38166  sge0rpcpnf  38171  meadjun  38208  meadjiunlem  38211  hoidmvlelem2  38322  usgrnloop1  39073