Theorem pm2.65da 671

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 670	1 |- ( ph -> -. ps )

This proof depends on syntax axioms:   -. wn 3   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108  ax-in1 623  ax-in2 624

This theorem is used by:  condandc  893  nelrdva  3033  ifnefals  3685  exmid01  4335  frirrg  4495  fimax2gtrilemstep  7205  unsnfidcex  7227  unsnfidcel  7228  difinfsn  7441  nninfisollemne  7472  fodju0  7488  nninfwlpoimlemginf  7517  exmidfodomrlemr  7555  exmidfodomrlemrALT  7556  exmidapne  7627  ltntri  8456  prodgt0  9185  ixxdisj  10316  icodisj  10405  zsupcllemstep  10673  infssuzex  10677  suprzubdc  10682  iseqf1olemnab  10953  seq3f1olemqsumk  10964  hashtpglem  11314  sq01  11676  ltabs  11870  divalglemnqt  12706  bitsfzolem  12740  bitsfzo  12741  sqnprm  12934  ballotfilem2  13280  ballotfilemfc0  13284  ballotfilemfcc  13285  ballotfilemimin  13301  ballotfilemic  13302  ballotfilem1c  13303  znnen  13341  aprnzr  14683  dedekindeulemuub  15809  dedekindeulemlu  15813  dedekindicclemuub  15818  dedekindicclemlu  15822  ivthinclemlopn  15828  ivthinclemuopn  15830  limcimo  15857  cnplimclemle  15860  pilem3  15976  logbgcd1irraplemexp  16165  mersenne  16258  bpos  16281  gausslemma2dlem1f1o  16345  umgrnloop2  16558  dichmul0orlem5  16923  dichmul0orlem6  16924  pw1ndom3lem  17185  pwtrufal  17193  pwle2  17194  peano3nninf  17216  nninffeq  17229  refeq  17239  trilpolemeq1  17256  taupi  17290