Theorem pm2.65da 662

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 661	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  882  nelrdva  2971  ifnefals  3603  exmid01  4231  frirrg  4385  fimax2gtrilemstep  6961  unsnfidcex  6981  unsnfidcel  6982  difinfsn  7166  nninfisollemne  7197  fodju0  7213  nninfwlpoimlemginf  7242  exmidfodomrlemr  7269  exmidfodomrlemrALT  7270  exmidapne  7327  ltntri  8154  prodgt0  8879  ixxdisj  9978  icodisj  10067  zsupcllemstep  10319  infssuzex  10323  suprzubdc  10326  iseqf1olemnab  10593  seq3f1olemqsumk  10604  ltabs  11252  divalglemnqt  12085  bitsfzolem  12118  bitsfzo  12119  sqnprm  12304  znnen  12615  dedekindeulemuub  14853  dedekindeulemlu  14857  dedekindicclemuub  14862  dedekindicclemlu  14866  ivthinclemlopn  14872  ivthinclemuopn  14874  limcimo  14901  cnplimclemle  14904  pilem3  15019  logbgcd1irraplemexp  15204  mersenne  15233  gausslemma2dlem1f1o  15301  pwtrufal  15642  pwle2  15643  peano3nninf  15651  nninffeq  15664  refeq  15672  trilpolemeq1  15684  taupi  15717