Theorem pm2.65da 667

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 666	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 619  ax-in2 620

This theorem is referenced by:  condandc  889  nelrdva  3014  ifnefals  3654  exmid01  4294  frirrg  4453  fimax2gtrilemstep  7133  unsnfidcex  7155  unsnfidcel  7156  difinfsn  7342  nninfisollemne  7373  fodju0  7389  nninfwlpoimlemginf  7418  exmidfodomrlemr  7456  exmidfodomrlemrALT  7457  exmidapne  7522  ltntri  8349  prodgt0  9074  ixxdisj  10182  icodisj  10271  zsupcllemstep  10535  infssuzex  10539  suprzubdc  10542  iseqf1olemnab  10809  seq3f1olemqsumk  10820  hashtpglem  11156  ltabs  11710  divalglemnqt  12544  bitsfzolem  12578  bitsfzo  12579  sqnprm  12771  znnen  13082  dedekindeulemuub  15411  dedekindeulemlu  15415  dedekindicclemuub  15420  dedekindicclemlu  15424  ivthinclemlopn  15430  ivthinclemuopn  15432  limcimo  15459  cnplimclemle  15462  pilem3  15577  logbgcd1irraplemexp  15762  mersenne  15794  gausslemma2dlem1f1o  15862  umgrnloop2  16075  pw1ndom3lem  16692  pwtrufal  16702  pwle2  16703  peano3nninf  16716  nninffeq  16729  refeq  16739  trilpolemeq1  16755  taupi  16789