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  4335  frirrg  4495  fimax2gtrilemstep  7205  unsnfidcex  7227  unsnfidcel  7228  difinfsn  7440  nninfisollemne  7471  fodju0  7487  nninfwlpoimlemginf  7516  exmidfodomrlemr  7554  exmidfodomrlemrALT  7555  exmidapne  7626  ltntri  8454  prodgt0  9182  ixxdisj  10305  icodisj  10394  zsupcllemstep  10662  infssuzex  10666  suprzubdc  10671  iseqf1olemnab  10938  seq3f1olemqsumk  10949  hashtpglem  11298  sq01  11660  ltabs  11853  divalglemnqt  12687  bitsfzolem  12721  bitsfzo  12722  sqnprm  12914  ballotfilem2  13228  ballotfilemfc0  13232  ballotfilemfcc  13233  ballotfilemimin  13249  ballotfilemic  13250  ballotfilem1c  13251  znnen  13289  aprnzr  14599  dedekindeulemuub  15718  dedekindeulemlu  15722  dedekindicclemuub  15727  dedekindicclemlu  15731  ivthinclemlopn  15737  ivthinclemuopn  15739  limcimo  15766  cnplimclemle  15769  pilem3  15884  logbgcd1irraplemexp  16070  mersenne  16111  gausslemma2dlem1f1o  16179  umgrnloop2  16392  dichmul0orlem5  16757  dichmul0orlem6  16758  pw1ndom3lem  17019  pwtrufal  17027  pwle2  17028  peano3nninf  17050  nninffeq  17063  refeq  17073  trilpolemeq1  17089  taupi  17123