Theorem pm2.65da 560

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

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

This theorem is referenced by:  condan  770  nelrdva  3103  onnseq  6565  oeeulem  6803  disjen  7223  cantnflem1  7601  ssfin4  8146  fin1a2lem12  8247  fin1a2lem13  8248  canthnumlem  8479  canthwelem  8481  supmul1  9929  ixxdisj  10887  ixxub  10893  ixxlb  10894  icodisj  10978  discr1  11470  sqrlem7  12009  bitsfzolem  12901  bitsfzo  12902  sqnprm  13053  mreexexlem2d  13825  acsinfd  14561  lbsextlem3  16187  lbsextlem4  16188  iuncon  17444  ptcmplem4  18039  iccntr  18805  evth  18937  bcthlem5  19234  ovolicopnf  19373  vitalilem4  19456  dvferm1  19822  dvferm2  19824  dgreq0  20136  radcnvle  20289  isosctrlem2  20616  mersenne  20964  pntlem3  21256  ostth2lem1  21265  ex-natded5.5  21671  ex-natded5.8  21674  ex-natded5.13  21676  qqhre  24339  ballotlemfc0  24703  ballotlemfcc  24704  ballotlemimin  24716  ballotlem1c  24718  dmlogdmgm  24761  supaddc  26137  bnj1417  29116

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8

This theorem depends on definitions:  df-bi 178  df-an 361