Theorem pm2.65da 662

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 661	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 615  ax-in2 616

This theorem is referenced by:  condandc  882  nelrdva  2968  ifnefals  3600  exmid01  4228  frirrg  4382  fimax2gtrilemstep  6958  unsnfidcex  6978  unsnfidcel  6979  difinfsn  7161  nninfisollemne  7192  fodju0  7208  nninfwlpoimlemginf  7237  exmidfodomrlemr  7264  exmidfodomrlemrALT  7265  exmidapne  7322  ltntri  8149  prodgt0  8873  ixxdisj  9972  icodisj  10061  iseqf1olemnab  10575  seq3f1olemqsumk  10586  ltabs  11234  divalglemnqt  12064  zsupcllemstep  12085  infssuzex  12089  suprzubdc  12092  sqnprm  12277  znnen  12558  dedekindeulemuub  14796  dedekindeulemlu  14800  dedekindicclemuub  14805  dedekindicclemlu  14809  ivthinclemlopn  14815  ivthinclemuopn  14817  limcimo  14844  cnplimclemle  14847  pilem3  14959  logbgcd1irraplemexp  15141  gausslemma2dlem1f1o  15217  pwtrufal  15558  pwle2  15559  peano3nninf  15567  nninffeq  15580  refeq  15588  trilpolemeq1  15600  taupi  15633