Theorem pm2.65da 651

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 114	. 2 |- ( ph -> ( ps -> ch ) )
3		pm2.65da.2	. . 3 |- ( ( ph /\ ps ) -> -. ch )
4	3	ex 114	. 2 |- ( ph -> ( ps -> -. ch ) )
5	2, 4	pm2.65d 650	1 |- ( ph -> -. ps )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107  ax-in1 604  ax-in2 605

This theorem is referenced by:  condandc  871  nelrdva  2932  exmid01  4176  frirrg  4327  fimax2gtrilemstep  6862  unsnfidcex  6881  unsnfidcel  6882  difinfsn  7061  nninfisollemne  7091  fodju0  7107  exmidfodomrlemr  7154  exmidfodomrlemrALT  7155  ltntri  8022  prodgt0  8743  ixxdisj  9835  icodisj  9924  iseqf1olemnab  10419  seq3f1olemqsumk  10430  ltabs  11025  divalglemnqt  11853  zsupcllemstep  11874  infssuzex  11878  suprzubdc  11881  sqnprm  12064  znnen  12327  dedekindeulemuub  13195  dedekindeulemlu  13199  dedekindicclemuub  13204  dedekindicclemlu  13208  ivthinclemlopn  13214  ivthinclemuopn  13216  limcimo  13234  cnplimclemle  13237  pilem3  13304  logbgcd1irraplemexp  13486  pwtrufal  13837  pwle2  13838  peano3nninf  13847  nninffeq  13860  refeq  13867  trilpolemeq1  13879  taupi  13909