Theorem pm2.65da 665

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 664	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 617  ax-in2 618

This theorem is referenced by:  condandc  886  nelrdva  3010  ifnefals  3647  exmid01  4282  frirrg  4441  fimax2gtrilemstep  7071  unsnfidcex  7093  unsnfidcel  7094  difinfsn  7278  nninfisollemne  7309  fodju0  7325  nninfwlpoimlemginf  7354  exmidfodomrlemr  7391  exmidfodomrlemrALT  7392  exmidapne  7457  ltntri  8285  prodgt0  9010  ixxdisj  10111  icodisj  10200  zsupcllemstep  10461  infssuzex  10465  suprzubdc  10468  iseqf1olemnab  10735  seq3f1olemqsumk  10746  ltabs  11613  divalglemnqt  12446  bitsfzolem  12480  bitsfzo  12481  sqnprm  12673  znnen  12984  dedekindeulemuub  15306  dedekindeulemlu  15310  dedekindicclemuub  15315  dedekindicclemlu  15319  ivthinclemlopn  15325  ivthinclemuopn  15327  limcimo  15354  cnplimclemle  15357  pilem3  15472  logbgcd1irraplemexp  15657  mersenne  15686  gausslemma2dlem1f1o  15754  umgrnloop2  15964  pw1ndom3lem  16412  pwtrufal  16422  pwle2  16423  peano3nninf  16433  nninffeq  16446  refeq  16456  trilpolemeq1  16468  taupi  16501