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  7281  exmidfodomrlemrALT  7282  exmidapne  7343  ltntri  8171  prodgt0  8896  ixxdisj  9995  icodisj  10084  zsupcllemstep  10336  infssuzex  10340  suprzubdc  10343  iseqf1olemnab  10610  seq3f1olemqsumk  10621  ltabs  11269  divalglemnqt  12102  bitsfzolem  12136  bitsfzo  12137  sqnprm  12329  znnen  12640  dedekindeulemuub  14937  dedekindeulemlu  14941  dedekindicclemuub  14946  dedekindicclemlu  14950  ivthinclemlopn  14956  ivthinclemuopn  14958  limcimo  14985  cnplimclemle  14988  pilem3  15103  logbgcd1irraplemexp  15288  mersenne  15317  gausslemma2dlem1f1o  15385  pwtrufal  15728  pwle2  15729  peano3nninf  15738  nninffeq  15751  refeq  15759  trilpolemeq1  15771  taupi  15804