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  2971  ifnefals  3604  exmid01  4232  frirrg  4386  fimax2gtrilemstep  6970  unsnfidcex  6990  unsnfidcel  6991  difinfsn  7175  nninfisollemne  7206  fodju0  7222  nninfwlpoimlemginf  7251  exmidfodomrlemr  7283  exmidfodomrlemrALT  7284  exmidapne  7345  ltntri  8173  prodgt0  8898  ixxdisj  9997  icodisj  10086  zsupcllemstep  10338  infssuzex  10342  suprzubdc  10345  iseqf1olemnab  10612  seq3f1olemqsumk  10623  ltabs  11271  divalglemnqt  12104  bitsfzolem  12138  bitsfzo  12139  sqnprm  12331  znnen  12642  dedekindeulemuub  14961  dedekindeulemlu  14965  dedekindicclemuub  14970  dedekindicclemlu  14974  ivthinclemlopn  14980  ivthinclemuopn  14982  limcimo  15009  cnplimclemle  15012  pilem3  15127  logbgcd1irraplemexp  15312  mersenne  15341  gausslemma2dlem1f1o  15409  pwtrufal  15752  pwle2  15753  peano3nninf  15762  nninffeq  15775  refeq  15785  trilpolemeq1  15797  taupi  15830