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

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

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  3313  onnseq  7015  oeeulem  7250  disjen  7674  cantnflem1  8108  cantnflem1OLD  8131  ssfin4  8690  fin1a2lem12  8791  fin1a2lem13  8792  canthnumlem  9026  canthwelem  9028  supmul1  10508  ixxdisj  11544  ixxub  11550  ixxlb  11551  icodisj  11645  discr1  12270  sqrlem7  13045  bitsfzolem  13943  bitsfzo  13944  sqnprm  14098  mreexexlem2d  14900  acsinfd  15667  lbsextlem3  17606  lbsextlem4  17607  iuncon  19723  ptcmplem4  20318  iccntr  21089  evth  21222  bcthlem5  21530  ovolicopnf  21698  vitalilem4  21783  dvferm1  22149  dvferm2  22151  dgreq0  22424  radcnvle  22577  isosctrlem2  22909  mersenne  23258  pntlem3  23550  ostth2lem1  23559  tgbtwnne  23637  tglowdim1i  23648  tgbtwndiff  23653  tgbtwnconn1lem3  23716  legso  23740  tglineintmo  23763  tglineneq  23765  tglowdim2ln  23773  krippenlem  23803  midexlem  23805  ragncol  23822  footex  23831  colperpexlem3  23839  mideulem  23841  lmieu  23855  ex-natded5.5  24836  ex-natded5.8  24839  ex-natded5.13  24841  nn0min  27307  ornglmullt  27488  orngrmullt  27489  qqhre  27662  oddpwdc  27961  eulerpartlemf  27977  ballotlemfc0  28099  ballotlemfcc  28100  ballotlemimin  28112  ballotlem1c  28114  dmlogdmgm  28234  supaddc  29646  ssnel  31029  limcperiod  31198  sumnnodd  31200  limclner  31221  icccncfext  31254  fperdvper  31276  dvdivbd  31281  dirkercncflem2  31432  fourierdlem10  31445  fourierdlem19  31454  fourierdlem20  31455  fourierdlem25  31460  fourierdlem35  31470  fourierdlem40  31475  fourierdlem41  31476  fourierdlem42  31477  fourierdlem46  31481  fourierdlem48  31483  fourierdlem49  31484  fourierdlem57  31492  fourierdlem58  31493  fourierdlem59  31494  fourierdlem63  31498  fourierdlem64  31499  fourierdlem65  31500  fourierdlem68  31503  fourierdlem74  31509  fourierdlem75  31510  fourierdlem78  31513  fourierdlem79  31514  fourierdlem80  31515  fourierswlem  31559  fouriersw  31560  iunconlem2  32833  bnj1417  33194