Theorem condan 835

Description: Proof by contradiction. (Contributed by NM, 9-Feb-2006.) (Proof shortened by Wolf Lammen, 19-Jun-2014.)

Hypotheses

Ref	Expression
condan.1	|- ( ( ph /\ -. ps ) -> ch )
condan.2	|- ( ( ph /\ -. ps ) -> -. ch )

Assertion

Ref	Expression
condan	|- ( ph -> ps )

Proof of Theorem condan

Step	Hyp	Ref	Expression
1		condan.1	. . 3 |- ( ( ph /\ -. ps ) -> ch )
2		condan.2	. . 3 |- ( ( ph /\ -. ps ) -> -. ch )
3	1, 2	pm2.65da 600	. 2 |- ( ph -> -. -. ps )
4	3	notnotrd 128	1 |- ( ph -> ps )

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386

This theorem is referenced by:  rlimcld2  14309  perfectlem2  24955  coltr  25542  2sqmod  29648  submomnd  29710  suborng  29815  ballotlemfc0  30554  ballotlemic  30568  unbdqndv2lem1  32500  disjf1  39369  mapssbi  39405  supxrgere  39549  supxrgelem  39553  supxrge  39554  xrlexaddrp  39568  reclt0d  39607  uzn0bi  39689  eliccnelico  39756  qinioo  39762  iccdificc  39766  sqrlearg  39780  fsumsupp0  39810  limcrecl  39861  limsuppnflem  39942  climisp  39978  climxlim2lem  40071  icccncfext  40100  stoweidlem52  40269  fourierdlem20  40344  fourierdlem34  40358  fourierdlem35  40359  fourierdlem38  40362  fourierdlem40  40364  fourierdlem41  40365  fourierdlem42  40366  fourierdlem46  40369  fourierdlem50  40373  fourierdlem60  40383  fourierdlem61  40384  fourierdlem64  40387  fourierdlem65  40388  fourierdlem72  40395  fourierdlem74  40397  fourierdlem75  40398  fourierdlem76  40399  fourierdlem78  40401  fouriersw  40448  elaa2lem  40450  etransclem24  40475  etransclem32  40483  etransclem35  40486  fge0iccico  40587  sge0cl  40598  sge0f1o  40599  sge0rernmpt  40639  meaiininclem  40700  hoidmv1lelem3  40807  hoidmvlelem2  40810  hoidmvlelem4  40812  hspmbllem2  40841  ovolval4lem1  40863  pimdecfgtioo  40927  pimincfltioo  40928  perfectALTVlem2  41631