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  3024  ifnefals  3667  exmid01  4311  frirrg  4471  fimax2gtrilemstep  7158  unsnfidcex  7180  unsnfidcel  7181  difinfsn  7391  nninfisollemne  7422  fodju0  7438  nninfwlpoimlemginf  7467  exmidfodomrlemr  7505  exmidfodomrlemrALT  7506  exmidapne  7574  ltntri  8401  prodgt0  9126  ixxdisj  10236  icodisj  10325  zsupcllemstep  10589  infssuzex  10593  suprzubdc  10596  iseqf1olemnab  10863  seq3f1olemqsumk  10874  hashtpglem  11218  ltabs  11772  divalglemnqt  12606  bitsfzolem  12640  bitsfzo  12641  sqnprm  12833  ballotfilem2  13142  znnen  13149  aprnzr  14433  dedekindeulemuub  15482  dedekindeulemlu  15486  dedekindicclemuub  15491  dedekindicclemlu  15495  ivthinclemlopn  15501  ivthinclemuopn  15503  limcimo  15530  cnplimclemle  15533  pilem3  15648  logbgcd1irraplemexp  15833  mersenne  15865  gausslemma2dlem1f1o  15933  umgrnloop2  16146  pw1ndom3lem  16763  pwtrufal  16771  pwle2  16772  peano3nninf  16785  nninffeq  16798  refeq  16808  trilpolemeq1  16824  taupi  16859