Theorem pm2.65da 667

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 666	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 619  ax-in2 620

This theorem is referenced by:  condandc  889  nelrdva  3027  ifnefals  3671  exmid01  4316  frirrg  4476  fimax2gtrilemstep  7171  unsnfidcex  7193  unsnfidcel  7194  difinfsn  7404  nninfisollemne  7435  fodju0  7451  nninfwlpoimlemginf  7480  exmidfodomrlemr  7518  exmidfodomrlemrALT  7519  exmidapne  7590  ltntri  8417  prodgt0  9143  ixxdisj  10255  icodisj  10344  zsupcllemstep  10611  infssuzex  10615  suprzubdc  10620  iseqf1olemnab  10887  seq3f1olemqsumk  10898  hashtpglem  11243  ltabs  11797  divalglemnqt  12631  bitsfzolem  12665  bitsfzo  12666  sqnprm  12858  ballotfilem2  13172  ballotfilemfc0  13176  ballotfilemfcc  13177  ballotfilemimin  13193  ballotfilemic  13194  ballotfilem1c  13195  znnen  13233  aprnzr  14537  dedekindeulemuub  15608  dedekindeulemlu  15612  dedekindicclemuub  15617  dedekindicclemlu  15621  ivthinclemlopn  15627  ivthinclemuopn  15629  limcimo  15656  cnplimclemle  15659  pilem3  15774  logbgcd1irraplemexp  15959  mersenne  15991  gausslemma2dlem1f1o  16059  umgrnloop2  16272  pw1ndom3lem  16889  pwtrufal  16897  pwle2  16898  peano3nninf  16911  nninffeq  16924  refeq  16934  trilpolemeq1  16950  taupi  16985