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  7440  nninfisollemne  7471  fodju0  7487  nninfwlpoimlemginf  7516  exmidfodomrlemr  7554  exmidfodomrlemrALT  7555  exmidapne  7626  ltntri  8455  prodgt0  9184  ixxdisj  10315  icodisj  10404  zsupcllemstep  10672  infssuzex  10676  suprzubdc  10681  iseqf1olemnab  10951  seq3f1olemqsumk  10962  hashtpglem  11312  sq01  11674  ltabs  11868  divalglemnqt  12703  bitsfzolem  12737  bitsfzo  12738  sqnprm  12931  ballotfilem2  13277  ballotfilemfc0  13281  ballotfilemfcc  13282  ballotfilemimin  13298  ballotfilemic  13299  ballotfilem1c  13300  znnen  13338  aprnzr  14648  dedekindeulemuub  15767  dedekindeulemlu  15771  dedekindicclemuub  15776  dedekindicclemlu  15780  ivthinclemlopn  15786  ivthinclemuopn  15788  limcimo  15815  cnplimclemle  15818  pilem3  15934  logbgcd1irraplemexp  16123  mersenne  16195  gausslemma2dlem1f1o  16277  umgrnloop2  16490  dichmul0orlem5  16855  dichmul0orlem6  16856  pw1ndom3lem  17117  pwtrufal  17125  pwle2  17126  peano3nninf  17148  nninffeq  17161  refeq  17171  trilpolemeq1  17187  taupi  17221