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  888  nelrdva  3013  ifnefals  3650  exmid01  4288  frirrg  4447  fimax2gtrilemstep  7090  unsnfidcex  7112  unsnfidcel  7113  difinfsn  7299  nninfisollemne  7330  fodju0  7346  nninfwlpoimlemginf  7375  exmidfodomrlemr  7413  exmidfodomrlemrALT  7414  exmidapne  7479  ltntri  8307  prodgt0  9032  ixxdisj  10138  icodisj  10227  zsupcllemstep  10490  infssuzex  10494  suprzubdc  10497  iseqf1olemnab  10764  seq3f1olemqsumk  10775  hashtpglem  11111  ltabs  11665  divalglemnqt  12499  bitsfzolem  12533  bitsfzo  12534  sqnprm  12726  znnen  13037  dedekindeulemuub  15360  dedekindeulemlu  15364  dedekindicclemuub  15369  dedekindicclemlu  15373  ivthinclemlopn  15379  ivthinclemuopn  15381  limcimo  15408  cnplimclemle  15411  pilem3  15526  logbgcd1irraplemexp  15711  mersenne  15740  gausslemma2dlem1f1o  15808  umgrnloop2  16021  pw1ndom3lem  16639  pwtrufal  16649  pwle2  16650  peano3nninf  16660  nninffeq  16673  refeq  16683  trilpolemeq1  16695  taupi  16729