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  7089  unsnfidcex  7111  unsnfidcel  7112  difinfsn  7298  nninfisollemne  7329  fodju0  7345  nninfwlpoimlemginf  7374  exmidfodomrlemr  7412  exmidfodomrlemrALT  7413  exmidapne  7478  ltntri  8306  prodgt0  9031  ixxdisj  10137  icodisj  10226  zsupcllemstep  10488  infssuzex  10492  suprzubdc  10495  iseqf1olemnab  10762  seq3f1olemqsumk  10773  ltabs  11647  divalglemnqt  12480  bitsfzolem  12514  bitsfzo  12515  sqnprm  12707  znnen  13018  dedekindeulemuub  15340  dedekindeulemlu  15344  dedekindicclemuub  15349  dedekindicclemlu  15353  ivthinclemlopn  15359  ivthinclemuopn  15361  limcimo  15388  cnplimclemle  15391  pilem3  15506  logbgcd1irraplemexp  15691  mersenne  15720  gausslemma2dlem1f1o  15788  umgrnloop2  16001  pw1ndom3lem  16588  pwtrufal  16598  pwle2  16599  peano3nninf  16609  nninffeq  16622  refeq  16632  trilpolemeq1  16644  taupi  16677