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  3168  onnseq  6805  oeeulem  7040  disjen  7468  cantnflem1  7897  cantnflem1OLD  7920  ssfin4  8479  fin1a2lem12  8580  fin1a2lem13  8581  canthnumlem  8815  canthwelem  8817  supmul1  10295  ixxdisj  11315  ixxub  11321  ixxlb  11322  icodisj  11410  discr1  12000  sqrlem7  12738  bitsfzolem  13630  bitsfzo  13631  sqnprm  13784  mreexexlem2d  14583  acsinfd  15350  lbsextlem3  17241  lbsextlem4  17242  iuncon  19032  ptcmplem4  19627  iccntr  20398  evth  20531  bcthlem5  20839  ovolicopnf  21007  vitalilem4  21091  dvferm1  21457  dvferm2  21459  dgreq0  21732  radcnvle  21885  isosctrlem2  22217  mersenne  22566  pntlem3  22858  ostth2lem1  22867  tglowdim1i  22954  tgbtwndiff  22959  tgbtwnconn1lem3  23006  tglineintmo  23047  tglineneq  23049  krippenlem  23084  midexlem  23086  ragncol  23102  footex  23109  ex-natded5.5  23617  ex-natded5.8  23620  ex-natded5.13  23622  nn0min  26090  ornglmullt  26275  orngrmullt  26276  qqhre  26446  oddpwdc  26737  eulerpartlemf  26753  ballotlemfc0  26875  ballotlemfcc  26876  ballotlemimin  26888  ballotlem1c  26890  dmlogdmgm  27010  supaddc  28417  iunconlem2  31671  bnj1417  32032