Theorem pm2.65da 661

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 660	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 614  ax-in2 615

This theorem is referenced by:  condandc  881  nelrdva  2946  exmid01  4200  frirrg  4352  fimax2gtrilemstep  6902  unsnfidcex  6921  unsnfidcel  6922  difinfsn  7101  nninfisollemne  7131  fodju0  7147  nninfwlpoimlemginf  7176  exmidfodomrlemr  7203  exmidfodomrlemrALT  7204  exmidapne  7261  ltntri  8087  prodgt0  8811  ixxdisj  9905  icodisj  9994  iseqf1olemnab  10490  seq3f1olemqsumk  10501  ltabs  11098  divalglemnqt  11927  zsupcllemstep  11948  infssuzex  11952  suprzubdc  11955  sqnprm  12138  znnen  12401  dedekindeulemuub  14180  dedekindeulemlu  14184  dedekindicclemuub  14189  dedekindicclemlu  14193  ivthinclemlopn  14199  ivthinclemuopn  14201  limcimo  14219  cnplimclemle  14222  pilem3  14289  logbgcd1irraplemexp  14471  pwtrufal  14832  pwle2  14833  peano3nninf  14841  nninffeq  14854  refeq  14861  trilpolemeq1  14873  taupi  14906