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  14134  dedekindeulemlu  14138  dedekindicclemuub  14143  dedekindicclemlu  14147  ivthinclemlopn  14153  ivthinclemuopn  14155  limcimo  14173  cnplimclemle  14176  pilem3  14243  logbgcd1irraplemexp  14425  pwtrufal  14786  pwle2  14787  peano3nninf  14795  nninffeq  14808  refeq  14815  trilpolemeq1  14827  taupi  14860