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 )

This proof depends on syntax axioms:   -. wn 3   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108  ax-in1 623  ax-in2 624

This theorem is used by:  condandc  893  nelrdva  3033  ifnefals  3685  exmid01  4337  frirrg  4497  fimax2gtrilemstep  7209  unsnfidcex  7231  unsnfidcel  7232  difinfsn  7446  nninfisollemne  7477  fodju0  7493  nninfwlpoimlemginf  7522  exmidfodomrlemr  7560  exmidfodomrlemrALT  7561  exmidapne  7632  ltntri  8461  prodgt0  9190  ixxdisj  10322  icodisj  10411  zsupcllemstep  10679  infssuzex  10683  suprzubdc  10688  iseqf1olemnab  10959  seq3f1olemqsumk  10970  hashtpglem  11320  sq01  11682  ltabs  11876  divalglemnqt  12712  bitsfzolem  12746  bitsfzo  12747  sqnprm  12940  ballotfilem2  13286  ballotfilemfc0  13290  ballotfilemfcc  13291  ballotfilemimin  13307  ballotfilemic  13308  ballotfilem1c  13309  znnen  13347  aprnzr  14708  dedekindeulemuub  15843  dedekindeulemlu  15847  dedekindicclemuub  15852  dedekindicclemlu  15856  ivthinclemlopn  15862  ivthinclemuopn  15864  limcimo  15891  cnplimclemle  15894  pilem3  16010  logbgcd1irraplemexp  16204  mersenne  16297  bpos  16320  gausslemma2dlem1f1o  16384  umgrnloop2  16597  dichmul0orlem5  16962  dichmul0orlem6  16963  pw1ndom3lem  17224  pwtrufal  17232  pwle2  17233  peano3nninf  17256  nninffeq  17269  refeq  17279  trilpolemeq1  17296  taupi  17330