Theorem pm2.65da 576

Description: Deduction rule for proof by contradiction. (Contributed by NM, 12-Jun-2014.)

Hypotheses

Ref	Expression
pm2.65da.1
pm2.65da.2

Assertion

Ref	Expression
pm2.65da

Proof of Theorem pm2.65da

Step	Hyp	Ref	Expression
1		pm2.65da.1	. . 3
2	1	ex 434	. 2
3		pm2.65da.2	. . 3
4	3	ex 434	. 2
5	2, 4	pm2.65d 175	1

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

This theorem is referenced by:  condan  794  nelrdva  3309  onnseq  7034  oeeulem  7269  disjen  7694  cantnflem1  8129  cantnflem1OLD  8152  ssfin4  8711  fin1a2lem12  8812  fin1a2lem13  8813  canthnumlem  9047  canthwelem  9049  supmul1  10533  ixxdisj  11573  ixxub  11579  ixxlb  11580  icodisj  11674  discr1  12302  sqrlem7  13082  bitsfzolem  14084  bitsfzo  14085  sqnprm  14239  mreexexlem2d  15042  acsinfd  15810  lbsextlem3  17806  lbsextlem4  17807  iuncon  19929  dissnlocfin  20030  ptcmplem4  20555  iccntr  21326  evth  21459  bcthlem5  21767  ovolicopnf  21935  vitalilem4  22020  dvferm1  22386  dvferm2  22388  dgreq0  22662  radcnvle  22815  isosctrlem2  23153  mersenne  23502  pntlem3  23794  ostth2lem1  23803  tgbtwnne  23881  tglowdim1i  23892  tgbtwndiff  23897  tgbtwnconn1lem3  23961  legso  23985  tglineintmo  24022  tglineneq  24024  tglowdim2ln  24032  mirhl  24059  krippenlem  24067  midexlem  24069  footex  24095  colperpexlem3  24106  mideulem2  24108  opphllem  24109  oppnid  24118  opphllem1  24119  opphllem2  24120  hpgerlem  24134  ex-natded5.5  25131  ex-natded5.8  25134  ex-natded5.13  25136  nn0min  27611  2sqn0  27634  ornglmullt  27797  orngrmullt  27798  qqhre  27998  oddpwdc  28293  eulerpartlemf  28309  ballotlemfc0  28431  ballotlemfcc  28432  ballotlemimin  28444  ballotlem1c  28446  dmlogdmgm  28566  supaddc  30041  n0p  31437  limclner  31657  icccncfext  31690  fperdvper  31715  dvdivbd  31720  dvdsn1add  31736  dvmptfprodlem  31741  dvnprodlem3  31745  fourierdlem10  31899  fourierdlem19  31908  fourierdlem20  31909  fourierdlem35  31924  fourierdlem40  31929  fourierdlem41  31930  fourierdlem42  31931  fourierdlem46  31935  fourierdlem48  31937  fourierdlem49  31938  fourierdlem57  31946  fourierdlem58  31947  fourierdlem59  31948  fourierdlem63  31952  fourierdlem64  31953  fourierdlem65  31954  fourierdlem68  31957  fourierdlem74  31963  fourierdlem75  31964  fourierdlem78  31967  fourierdlem79  31968  fourierdlem80  31969  elaa2  32017  etransclem35  32052  etransclem38  32055  iunconlem2  33735  bnj1417  34097  imo72b2  37993

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