Theorem pm2.65da 573

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  787  nelrdva  3161  onnseq  6795  oeeulem  7032  disjen  7460  cantnflem1  7889  cantnflem1OLD  7912  ssfin4  8471  fin1a2lem12  8572  fin1a2lem13  8573  canthnumlem  8807  canthwelem  8809  supmul1  10287  ixxdisj  11307  ixxub  11313  ixxlb  11314  icodisj  11401  discr1  11988  sqrlem7  12726  bitsfzolem  13617  bitsfzo  13618  sqnprm  13771  mreexexlem2d  14570  acsinfd  15337  lbsextlem3  17167  lbsextlem4  17168  iuncon  18878  ptcmplem4  19473  iccntr  20244  evth  20377  bcthlem5  20685  ovolicopnf  20853  vitalilem4  20937  dvferm1  21303  dvferm2  21305  dgreq0  21621  radcnvle  21774  isosctrlem2  22106  mersenne  22455  pntlem3  22747  ostth2lem1  22756  tglowdim1i  22840  tgbtwndiff  22845  tgbtwnconn1lem3  22886  tglineintmo  22921  ex-natded5.5  23444  ex-natded5.8  23447  ex-natded5.13  23449  nn0min  25917  ornglmullt  26132  orngrmullt  26133  qqhre  26304  oddpwdc  26589  eulerpartlemf  26605  ballotlemfc0  26727  ballotlemfcc  26728  ballotlemimin  26740  ballotlem1c  26742  dmlogdmgm  26862  supaddc  28265  iunconlem2  31436  bnj1417  31797