Theorem pm2.65da 600

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 450	. 2 |- ( ph -> ( ps -> ch ) )
3		pm2.65da.2	. . 3 |- ( ( ph /\ ps ) -> -. ch )
4	3	ex 450	. 2 |- ( ph -> ( ps -> -. ch ) )
5	2, 4	pm2.65d 187	1 |- ( ph -> -. ps )

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

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 197  df-an 386

This theorem is referenced by:  condan  835  nelrdva  3417  onnseq  7441  oeeulem  7681  disjen  8117  cantnflem1  8586  ssfin4  9132  fin1a2lem12  9233  fin1a2lem13  9234  canthnumlem  9470  canthwelem  9472  supaddc  10990  supmul1  10992  ixxdisj  12190  ixxub  12196  ixxlb  12197  icodisj  12297  discr1  13000  sqrlem7  13989  bitsfzolem  15156  bitsfzo  15157  sqnprm  15414  mreexexlem2d  16305  acsinfd  17180  lbsextlem3  19160  lbsextlem4  19161  iunconn  21231  dissnlocfin  21332  ptcmplem4  21859  iccntr  22624  evth  22758  bcthlem5  23125  ovolicopnf  23292  vitalilem4  23380  dvferm1  23748  dvferm2  23750  dgreq0  24021  radcnvle  24174  isosctrlem2  24549  dmlogdmgm  24750  mersenne  24952  pntlem3  25298  ostth2lem1  25307  tgbtwnne  25385  tglowdim1i  25396  tgbtwndiff  25401  tgbtwnconn1lem3  25469  legso  25494  tglineintmo  25537  tglineneq  25539  tglowdim2ln  25546  mirne  25562  mirhl  25574  krippenlem  25585  midexlem  25587  footex  25613  colperpexlem3  25624  mideulem2  25626  opphllem  25627  oppne3  25635  oppnid  25638  opphllem1  25639  opphllem2  25640  outpasch  25647  hlpasch  25648  hpgerlem  25657  colhp  25662  trgcopy  25696  cgrancol  25720  tgasa1  25739  umgrnloop2  26041  ex-natded5.5  27267  ex-natded5.8  27270  ex-natded5.13  27272  nn0min  29567  2sqn0  29646  ornglmullt  29807  orngrmullt  29808  qqhre  30064  esumcvgre  30153  carsgclctunlem2  30381  oddpwdc  30416  eulerpartlemf  30432  ballotlemfc0  30554  ballotlemfcc  30555  ballotlemimin  30567  ballotlem1c  30569  reprinfz1  30700  bnj1417  31109  unbdqndv2lem2  32501  knoppndvlem13  32515  topdifinffinlem  33195  poimirlem11  33420  poimirlem12  33421  imo72b2  38475  iunconnlem2  39171  n0p  39209  uzwo4  39221  ssnct  39249  nsstr  39273  disjrnmpt2  39375  difmap  39399  difmapsn  39404  mapssbi  39405  xrlexaddrp  39568  infleinflem2  39587  xrralrecnnge  39613  supminfxr2  39699  icoub  39752  ioonct  39764  ressioosup  39782  ressiooinf  39784  limclner  39883  limsupub  39936  climxrrelem  39981  climlimsupcex  40001  icccncfext  40100  fperdvper  40133  dvdivbd  40138  dvdsn1add  40154  dvmptfprodlem  40159  dvnprodlem3  40163  fourierdlem10  40334  fourierdlem19  40343  fourierdlem20  40344  fourierdlem35  40359  fourierdlem40  40364  fourierdlem41  40365  fourierdlem42  40366  fourierdlem46  40369  fourierdlem48  40371  fourierdlem49  40372  fourierdlem57  40380  fourierdlem58  40381  fourierdlem59  40382  fourierdlem63  40386  fourierdlem64  40387  fourierdlem65  40388  fourierdlem68  40391  fourierdlem74  40397  fourierdlem75  40398  fourierdlem78  40401  fourierdlem79  40402  fourierdlem80  40403  elaa2  40451  etransclem35  40486  etransclem38  40489  prsal  40538  fge0npnf  40584  sge0tsms  40597  sge0rern  40605  sge0supre  40606  sge0le  40624  sge0fodjrnlem  40633  sge0rpcpnf  40638  meadjun  40679  meadjiunlem  40682  hoidmvlelem2  40810  hspdifhsp  40830  ovolval4lem1  40863  preimagelt  40912  preimalegt  40913