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  2979  ifnefals  3613  exmid01  4241  frirrg  4395  fimax2gtrilemstep  6979  unsnfidcex  6999  unsnfidcel  7000  difinfsn  7184  nninfisollemne  7215  fodju0  7231  nninfwlpoimlemginf  7260  exmidfodomrlemr  7292  exmidfodomrlemrALT  7293  exmidapne  7354  ltntri  8182  prodgt0  8907  ixxdisj  10007  icodisj  10096  zsupcllemstep  10353  infssuzex  10357  suprzubdc  10360  iseqf1olemnab  10627  seq3f1olemqsumk  10638  ltabs  11317  divalglemnqt  12150  bitsfzolem  12184  bitsfzo  12185  sqnprm  12377  znnen  12688  dedekindeulemuub  15007  dedekindeulemlu  15011  dedekindicclemuub  15016  dedekindicclemlu  15020  ivthinclemlopn  15026  ivthinclemuopn  15028  limcimo  15055  cnplimclemle  15058  pilem3  15173  logbgcd1irraplemexp  15358  mersenne  15387  gausslemma2dlem1f1o  15455  pwtrufal  15798  pwle2  15799  peano3nninf  15808  nninffeq  15821  refeq  15831  trilpolemeq1  15843  taupi  15876