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  7211  unsnfidcex  7233  unsnfidcel  7234  difinfsn  7446  nninfisollemne  7477  fodju0  7493  nninfwlpoimlemginf  7522  exmidfodomrlemr  7560  exmidfodomrlemrALT  7561  exmidapne  7632  ltntri  8461  prodgt0  9190  ixxdisj  10321  icodisj  10410  zsupcllemstep  10678  infssuzex  10682  suprzubdc  10687  iseqf1olemnab  10958  seq3f1olemqsumk  10969  hashtpglem  11319  sq01  11681  ltabs  11875  divalglemnqt  12711  bitsfzolem  12745  bitsfzo  12746  sqnprm  12939  ballotfilem2  13285  ballotfilemfc0  13289  ballotfilemfcc  13290  ballotfilemimin  13306  ballotfilemic  13307  ballotfilem1c  13308  znnen  13346  aprnzr  14707  dedekindeulemuub  15860  dedekindeulemlu  15864  dedekindicclemuub  15869  dedekindicclemlu  15873  ivthinclemlopn  15879  ivthinclemuopn  15881  limcimo  15908  cnplimclemle  15911  pilem3  16027  logbgcd1irraplemexp  16221  mersenne  16314  bpos  16337  gausslemma2dlem1f1o  16401  umgrnloop2  16614  dichmul0orlem5  16979  dichmul0orlem6  16980  pw1ndom3lem  17241  pwtrufal  17249  pwle2  17250  peano3nninf  17273  nninffeq  17286  refeq  17296  trilpolemeq1  17313  taupi  17347