Theorem pm2.65da 671

Description: Deduction 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 115	. 2 |- ( ph -> ( ps -> ch ) )
3		pm2.65da.2	. . 3 |- ( ( ph /\ ps ) -> -. ch )
4	3	ex 115	. 2 |- ( ph -> ( ps -> -. ch ) )
5	2, 4	pm2.65d 670	1 |- ( ph -> -. ps )

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108  ax-in1 623  ax-in2 624

This theorem is referenced by:  condandc  893  nelrdva  3033  ifnefals  3682  exmid01  4330  frirrg  4490  fimax2gtrilemstep  7195  unsnfidcex  7217  unsnfidcel  7218  difinfsn  7430  nninfisollemne  7461  fodju0  7477  nninfwlpoimlemginf  7506  exmidfodomrlemr  7544  exmidfodomrlemrALT  7545  exmidapne  7616  ltntri  8444  prodgt0  9172  ixxdisj  10284  icodisj  10373  zsupcllemstep  10640  infssuzex  10644  suprzubdc  10649  iseqf1olemnab  10916  seq3f1olemqsumk  10927  hashtpglem  11276  sq01  11638  ltabs  11831  divalglemnqt  12665  bitsfzolem  12699  bitsfzo  12700  sqnprm  12892  ballotfilem2  13206  ballotfilemfc0  13210  ballotfilemfcc  13211  ballotfilemimin  13227  ballotfilemic  13228  ballotfilem1c  13229  znnen  13267  aprnzr  14572  dedekindeulemuub  15641  dedekindeulemlu  15645  dedekindicclemuub  15650  dedekindicclemlu  15654  ivthinclemlopn  15660  ivthinclemuopn  15662  limcimo  15689  cnplimclemle  15692  pilem3  15807  logbgcd1irraplemexp  15993  mersenne  16025  gausslemma2dlem1f1o  16093  umgrnloop2  16306  dichmul0orlem5  16671  dichmul0orlem6  16672  pw1ndom3lem  16933  pwtrufal  16941  pwle2  16942  peano3nninf  16955  nninffeq  16968  refeq  16978  trilpolemeq1  16994  taupi  17028