Theorem pm2.65da 663

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 662	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  883  nelrdva  2984  ifnefals  3619  exmid01  4250  frirrg  4405  fimax2gtrilemstep  7012  unsnfidcex  7032  unsnfidcel  7033  difinfsn  7217  nninfisollemne  7248  fodju0  7264  nninfwlpoimlemginf  7293  exmidfodomrlemr  7326  exmidfodomrlemrALT  7327  exmidapne  7392  ltntri  8220  prodgt0  8945  ixxdisj  10045  icodisj  10134  zsupcllemstep  10394  infssuzex  10398  suprzubdc  10401  iseqf1olemnab  10668  seq3f1olemqsumk  10679  ltabs  11473  divalglemnqt  12306  bitsfzolem  12340  bitsfzo  12341  sqnprm  12533  znnen  12844  dedekindeulemuub  15164  dedekindeulemlu  15168  dedekindicclemuub  15173  dedekindicclemlu  15177  ivthinclemlopn  15183  ivthinclemuopn  15185  limcimo  15212  cnplimclemle  15215  pilem3  15330  logbgcd1irraplemexp  15515  mersenne  15544  gausslemma2dlem1f1o  15612  pwtrufal  16075  pwle2  16076  peano3nninf  16085  nninffeq  16098  refeq  16108  trilpolemeq1  16120  taupi  16153