Theorem pm2.65da 584

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

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

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 190  df-an 377

This theorem is referenced by:  condan  808  nelrdva  3217  onnseq  7050  oeeulem  7289  disjen  7716  cantnflem1  8181  ssfin4  8727  fin1a2lem12  8828  fin1a2lem13  8829  canthnumlem  9060  canthwelem  9062  supaddc  10563  supmul1  10565  ixxdisj  11640  ixxub  11646  ixxlb  11647  ixxlbOLD  11648  icodisj  11748  discr1  12402  sqrlem7  13323  bitsfzolem  14418  bitsfzolemOLD  14419  bitsfzo  14420  sqnprm  14657  mreexexlem2d  15562  acsinfd  16437  lbsextlem3  18394  lbsextlem4  18395  iuncon  20454  dissnlocfin  20555  ptcmplem4  21081  iccntr  21850  evth  21998  bcthlem5  22307  ovolicopnf  22489  vitalilem4  22581  dvferm1  22949  dvferm2  22951  dgreq0  23231  radcnvle  23387  isosctrlem2  23760  dmlogdmgm  23961  mersenne  24167  pntlem3  24459  ostth2lem1  24468  tgbtwnne  24546  tglowdim1i  24557  tgbtwndiff  24562  tgbtwnconn1lem3  24631  legso  24656  tglineintmo  24699  tglineneq  24701  tglowdim2ln  24708  mirne  24724  mirhl  24736  krippenlem  24747  midexlem  24749  footex  24775  colperpexlem3  24786  mideulem2  24788  opphllem  24789  oppne3  24797  oppnid  24800  opphllem1  24801  opphllem2  24802  outpasch  24809  hlpasch  24810  hpgerlem  24819  colhp  24824  trgcopy  24858  cgrancol  24882  tgasa1  24901  ex-natded5.5  25872  ex-natded5.8  25875  ex-natded5.13  25877  nn0min  28392  2sqn0  28415  ornglmullt  28577  orngrmullt  28578  qqhre  28831  esumcvgre  28919  carsgclctunlem2  29157  oddpwdc  29193  eulerpartlemf  29209  ballotlemfc0  29331  ballotlemfcc  29332  ballotlemimin  29344  ballotlem1c  29346  ballotlemiminOLD  29382  ballotlem1cOLD  29384  bnj1417  29856  topdifinffinlem  31752  poimirlem11  31953  poimirlem12  31954  imo72b2  36620  iunconlem2  37329  n0p  37371  uzwo4  37387  ssnct  37420  nelpr2  37435  nelpr1  37436  disjrnmpt2  37473  difmap  37499  difmapsn  37506  mapssbi  37507  xrlexaddrp  37606  infleinflem2  37626  icoub  37668  ioonct  37680  limclner  37774  icccncfext  37807  fperdvper  37832  dvdivbd  37837  dvdsn1add  37856  dvmptfprodlem  37861  dvnprodlem3  37865  fourierdlem10  38036  fourierdlem19  38045  fourierdlem20  38046  fourierdlem35  38062  fourierdlem40  38067  fourierdlem41  38068  fourierdlem42  38069  fourierdlem42OLD  38070  fourierdlem46  38073  fourierdlem48  38075  fourierdlem49  38076  fourierdlem57  38084  fourierdlem58  38085  fourierdlem59  38086  fourierdlem63  38090  fourierdlem64  38091  fourierdlem65  38092  fourierdlem68  38095  fourierdlem74  38101  fourierdlem75  38102  fourierdlem78  38105  fourierdlem79  38106  fourierdlem80  38107  elaa2  38156  etransclem35  38191  etransclem38  38194  prsal  38236  fge0npnf  38268  sge0tsms  38281  sge0rern  38289  sge0supre  38290  sge0le  38308  sge0fodjrnlem  38317  sge0rpcpnf  38322  meadjun  38361  meadjiunlem  38364  hoidmvlelem2  38481  hspdifhsp  38501  ovolval4lem1  38534  umgrnloop2  39334