Theorem pm2.65da 574

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

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

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 369

This theorem is referenced by:  condan  792  nelrdva  3234  onnseq  6933  oeeulem  7168  disjen  7593  cantnflem1  8021  cantnflem1OLD  8044  ssfin4  8603  fin1a2lem12  8704  fin1a2lem13  8705  canthnumlem  8937  canthwelem  8939  supmul1  10424  ixxdisj  11465  ixxub  11471  ixxlb  11472  icodisj  11566  discr1  12204  sqrlem7  13084  bitsfzolem  14086  bitsfzo  14087  sqnprm  14241  mreexexlem2d  15052  acsinfd  15927  lbsextlem3  17919  lbsextlem4  17920  iuncon  20014  dissnlocfin  20115  ptcmplem4  20640  iccntr  21411  evth  21544  bcthlem5  21852  ovolicopnf  22020  vitalilem4  22105  dvferm1  22471  dvferm2  22473  dgreq0  22747  radcnvle  22900  isosctrlem2  23269  mersenne  23619  pntlem3  23911  ostth2lem1  23920  tgbtwnne  24001  tglowdim1i  24012  tgbtwndiff  24017  tgbtwnconn1lem3  24081  legso  24105  tglineintmo  24142  tglineneq  24144  tglowdim2ln  24152  mirhl  24179  krippenlem  24187  midexlem  24189  footex  24215  colperpexlem3  24226  mideulem2  24228  opphllem  24229  oppnid  24238  opphllem1  24239  opphllem2  24240  hpgerlem  24254  cgraid  24290  ex-natded5.5  25252  ex-natded5.8  25255  ex-natded5.13  25257  nn0min  27764  2sqn0  27787  ornglmullt  27951  orngrmullt  27952  qqhre  28151  esumcvgre  28239  carsgclctunlem2  28446  oddpwdc  28476  eulerpartlemf  28492  ballotlemfc0  28614  ballotlemfcc  28615  ballotlemimin  28627  ballotlem1c  28629  dmlogdmgm  28755  supaddc  30206  n0p  31604  limclner  31823  icccncfext  31856  fperdvper  31881  dvdivbd  31886  dvdsn1add  31902  dvmptfprodlem  31907  dvnprodlem3  31911  fourierdlem10  32065  fourierdlem19  32074  fourierdlem20  32075  fourierdlem35  32090  fourierdlem40  32095  fourierdlem41  32096  fourierdlem42  32097  fourierdlem46  32101  fourierdlem48  32103  fourierdlem49  32104  fourierdlem57  32112  fourierdlem58  32113  fourierdlem59  32114  fourierdlem63  32118  fourierdlem64  32119  fourierdlem65  32120  fourierdlem68  32123  fourierdlem74  32129  fourierdlem75  32130  fourierdlem78  32133  fourierdlem79  32134  fourierdlem80  32135  elaa2  32183  etransclem35  32218  etransclem38  32221  iunconlem2  34082  bnj1417  34444  imo72b2  38522