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  4281  frirrg  4440  fimax2gtrilemstep  7058  unsnfidcex  7078  unsnfidcel  7079  difinfsn  7263  nninfisollemne  7294  fodju0  7310  nninfwlpoimlemginf  7339  exmidfodomrlemr  7376  exmidfodomrlemrALT  7377  exmidapne  7442  ltntri  8270  prodgt0  8995  ixxdisj  10095  icodisj  10184  zsupcllemstep  10444  infssuzex  10448  suprzubdc  10451  iseqf1olemnab  10718  seq3f1olemqsumk  10729  ltabs  11593  divalglemnqt  12426  bitsfzolem  12460  bitsfzo  12461  sqnprm  12653  znnen  12964  dedekindeulemuub  15285  dedekindeulemlu  15289  dedekindicclemuub  15294  dedekindicclemlu  15298  ivthinclemlopn  15304  ivthinclemuopn  15306  limcimo  15333  cnplimclemle  15336  pilem3  15451  logbgcd1irraplemexp  15636  mersenne  15665  gausslemma2dlem1f1o  15733  umgrnloop2  15943  pwtrufal  16322  pwle2  16323  peano3nninf  16332  nninffeq  16345  refeq  16355  trilpolemeq1  16367  taupi  16400