Theorem pm2.61dan 832

Description: Elimination of an antecedent. (Contributed by NM, 1-Jan-2005.)

Hypotheses

Ref	Expression
pm2.61dan.1	|- ( ( ph /\ ps ) -> ch )
pm2.61dan.2	|- ( ( ph /\ -. ps ) -> ch )

Assertion

Ref	Expression
pm2.61dan	|- ( ph -> ch )

Proof of Theorem pm2.61dan

Step	Hyp	Ref	Expression
1		pm2.61dan.1	. . 3 |- ( ( ph /\ ps ) -> ch )
2	1	ex 450	. 2 |- ( ph -> ( ps -> ch ) )
3		pm2.61dan.2	. . 3 |- ( ( ph /\ -. ps ) -> ch )
4	3	ex 450	. 2 |- ( ph -> ( -. ps -> ch ) )
5	2, 4	pm2.61d 170	1 |- ( ph -> ch )

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:  pm2.61ddan  833  pm2.61dda  834  nfsb4t  2389  pm2.61danel  2911  ifeq1da  4116  ifeq2da  4117  ifeq12da  4118  ifclda  4120  ifeqda  4121  ifbothda  4123  2if2  4136  nelsnOLD  4213  somin1  5529  xpcan  5570  fvmpti  6281  fvmptss  6292  funressn  6426  ovima0  6813  oeoa  7677  oeoe  7679  omabs  7727  eceqoveq  7853  domdifsn  8043  pw2f1olem  8064  mapdom1  8125  marypha1lem  8339  supval2  8361  infdifsn  8554  carden2b  8793  fidomtri  8819  dfac12lem2  8966  cdadom1  9008  infunsdom1  9035  infunsdom  9036  itunisuc  9241  gchdomtri  9451  xrmax2  12007  xrmin1  12008  ifle  12028  xmulneg1  12099  xrsupsslem  12137  xrinfmsslem  12138  fzneuz  12421  seqf1olem1  12840  bccmpl  13096  bcval5  13105  bcpasc  13108  bccl  13109  hasheni  13136  hashfn  13164  hashdom  13168  hashdomi  13169  hashge1  13178  hashbc  13237  sumz  14453  sumss  14455  fsumsplitsn  14474  sumsplit  14499  prod1  14674  prodss  14677  fprodsplitsn  14720  fprodle  14727  bitsmod  15158  sadadd2lem2  15172  sadcaddlem  15179  gcddvds  15225  gcdcl  15228  gcdneg  15243  dvdslcm  15311  lcmcl  15314  lcmneg  15316  lcmgcd  15320  lcmfcl  15341  dvdslcmf  15344  pcgcd  15582  pcmpt  15596  pcmpt2  15597  pcprod  15599  fldivp1  15601  prmreclem4  15623  vdwlem6  15690  ramub1lem1  15730  cidpropd  16370  rescabs  16493  lubval  16984  glbval  16997  joinval  17005  meetval  17019  acsexdimd  17183  gsumpropd2lem  17273  gsumval2  17280  f1otrspeq  17867  pmtrfinv  17881  psgnunilem1  17913  gsumval3  18308  ablfac1c  18470  ablfac1eu  18472  mgpress  18500  psrbas  19378  resspsrbas  19415  mplmonmul  19464  mplcoe1  19465  mplcoe5  19468  opsrle  19475  opsrbaslem  19477  opsrbaslemOLD  19478  psrbaspropd  19605  mplbaspropd  19607  frlmsslsp  20135  mdetdiag  20405  mdetunilem7  20424  mdetunilem9  20426  maducoeval2  20446  madurid  20450  opnnei  20924  restbas  20962  hauspwdom  21304  ptcmplem5  21860  xrsmopn  22615  xrhmeo  22745  lebnum  22763  pcohtpylem  22819  pcoass  22824  pcorevlem  22826  icombl  23332  ioombl  23333  mbfconstlem  23396  mbfima  23399  i1fd  23448  mbfi1fseqlem5  23486  itg2const2  23508  itg2seq  23509  itg2uba  23510  itg2splitlem  23515  itg2split  23516  itg2monolem1  23517  itg2gt0  23527  itg2cnlem1  23528  itg2cnlem2  23529  iblss  23571  iblss2  23572  itgss  23578  bddmulibl  23605  coemullem  24006  aaliou2b  24096  isppw2  24841  mule1  24874  ppip1le  24887  dchrelbas3  24963  dchrpt  24992  bposlem3  25011  bposlem5  25013  bposlem6  25014  lgslem4  25025  lgsneg  25046  lgsmod  25048  lgsdilem  25049  lgsdir  25057  lgsdi  25059  lgsne0  25060  lgsquad3  25112  dchrvmasum2if  25186  midexlem  25587  colperpex  25625  outpasch  25647  hlpasch  25648  lnopp2hpgb  25655  lmieu  25676  inaghl  25731  cgrg3col4  25734  pthdlem1  26662  nmcfnlbi  28911  elpreq  29360  disjdifprg  29388  disjun0  29408  f1ocnt  29559  xrge0npcan  29694  archiabl  29752  orngsqr  29804  psgnfzto1stlem  29850  1smat1  29870  esumcst  30125  esumrnmpt2  30130  hasheuni  30147  esumcvg  30148  ddemeas  30299  omssubadd  30362  eulerpartlemgc  30424  eulerpartlemb  30430  plymulx  30625  signswmnd  30634  signstfvneq0  30649  erdsze2lem1  31185  mrsubvrs  31419  trpredlem1  31727  unblimceq0lem  32497  unbdqndv2lem2  32501  knoppndvlem10  32512  wl-spae  33306  wl-cbvalnaed  33319  wl-nfeqfb  33323  unccur  33392  poimirlem15  33424  poimirlem22  33431  itg2addnclem  33461  itg2addnclem2  33462  iblmulc2nc  33475  ftc1anclem5  33489  ftc1anc  33493  dvasin  33496  areacirclem5  33504  exmid2  33901  3dim1  34753  3dim2  34754  3dim3  34755  3atlem3  34771  3atlem7  34775  lvolnle3at  34868  2lplnja  34905  paddasslem18  35123  lhpexle3lem  35297  4atex  35362  cdlemd5  35489  cdleme16  35572  cdleme20  35612  cdleme21j  35624  cdleme21  35625  cdleme32snaw  35723  cdleme32fvcl  35728  cdleme32le  35735  cdlemeg46gf  35821  cdleme48gfv  35825  cdleme50trn12  35840  cdlemg6  35911  cdlemg7N  35914  cdlemg38  36003  cdlemg46  36023  dibvalrel  36452  dihlss  36539  dihglblem5aN  36581  dihmeetbN  36592  dihmeetALTN  36616  dihatlat  36623  dihatexv  36627  dvh3dim2  36737  dvh3dim3N  36738  lclkrlem2h  36803  mapdh8d  37072  mapdh8g  37075  hdmap11lem2  37134  ttac  37603  pw2f1ocnv  37604  aomclem5  37628  isnumbasgrplem3  37675  iocmbl  37798  radcnvrat  38513  bccbc  38544  binomcxp  38556  fnchoice  39188  fiiuncl  39234  disjxp1  39238  eliin2f  39287  founiiun0  39377  axccdom  39416  axccd2  39430  fzisoeu  39514  fperiodmul  39518  upbdrech2  39522  fzdifsuc2  39525  uzfissfz  39542  supxrgere  39549  supxrgelem  39553  supxrge  39554  suplesup  39555  infrpge  39567  xrlexaddrp  39568  xralrple2  39570  infxr  39583  infleinflem1  39586  infleinflem2  39587  infleinf  39588  xralrple3  39590  fiminre2  39594  xrralrecnnge  39613  uzublem  39657  supxrmnf2  39660  infxrpnf  39674  infxrpnf2  39693  supminfxr  39694  supminfxr2  39699  ioondisj2  39714  iccdifprioo  39742  fmul01lt1lem1  39816  fmul01lt1lem2  39817  limciccioolb  39853  lptioo2  39863  lptioo1  39864  limcicciooub  39869  lptre2pt  39872  limcresiooub  39874  limcresioolb  39875  limcleqr  39876  climfveq  39901  climfveqf  39912  limsupubuzlem  39944  limsupubuz  39945  limsupmnfuzlem  39958  limsupre3uzlem  39967  climxrre  39982  limsup10exlem  40004  cnrefiisplem  40055  climxlim2lem  40071  dfxlim2v  40073  coskpi2  40077  cosknegpi  40080  icccncfext  40100  cncfiooicclem1  40106  cncfiooicc  40107  cncfiooiccre  40108  dvbdfbdioolem2  40144  ioodvbdlimc1lem1  40146  ioodvbdlimc1lem2  40147  ioodvbdlimc2lem  40149  dvnxpaek  40157  dvnprodlem1  40161  dvnprodlem3  40163  volioc  40188  itgioocnicc  40193  iblcncfioo  40194  volico  40200  sublevolico  40201  ismbl3  40203  ovolsplit  40205  volioore  40207  voliooico  40209  voliccico  40216  stoweidlem14  40231  stoweidlem26  40243  stoweidlem28  40245  stoweidlem55  40272  stoweid  40280  stirlinglem5  40295  stirlinglem12  40302  dirkerper  40313  dirkertrigeqlem3  40317  dirkertrigeq  40318  dirkercncflem1  40320  dirkercncflem2  40321  dirkercncf  40324  fourierdlem10  40334  fourierdlem12  40336  fourierdlem24  40348  fourierdlem30  40354  fourierdlem31  40355  fourierdlem32  40356  fourierdlem33  40357  fourierdlem34  40358  fourierdlem35  40359  fourierdlem37  40361  fourierdlem40  40364  fourierdlem41  40365  fourierdlem42  40366  fourierdlem43  40367  fourierdlem44  40368  fourierdlem46  40369  fourierdlem48  40371  fourierdlem49  40372  fourierdlem51  40374  fourierdlem54  40377  fourierdlem62  40385  fourierdlem64  40387  fourierdlem65  40388  fourierdlem70  40393  fourierdlem71  40394  fourierdlem73  40396  fourierdlem74  40397  fourierdlem75  40398  fourierdlem78  40401  fourierdlem79  40402  fourierdlem80  40403  fourierdlem81  40404  fourierdlem82  40405  fourierdlem92  40415  fourierdlem93  40416  fourierdlem97  40420  fourierdlem101  40424  fourierdlem102  40425  fourierdlem103  40426  fourierdlem104  40427  fourierdlem109  40432  fourierdlem114  40437  sqwvfoura  40445  sqwvfourb  40446  fourierswlem  40447  fouriersw  40448  elaa2lem  40450  etransclem15  40466  etransclem19  40470  etransclem20  40471  etransclem22  40473  etransclem23  40474  etransclem24  40475  etransclem25  40476  etransclem27  40478  etransclem28  40479  etransclem35  40486  etransclem38  40489  qndenserrnbl  40515  ioorrnopn  40525  ioorrnopnxrlem  40526  ioorrnopnxr  40527  prsal  40538  salexct  40552  issalnnd  40563  sge0sn  40596  sge0tsms  40597  sge0cl  40598  sge0f1o  40599  sge0sup  40608  sge0less  40609  sge0pr  40611  sge0prle  40618  sge0le  40624  sge0split  40626  sge0splitmpt  40628  sge0iunmptlemfi  40630  sge0iunmpt  40635  sge0isum  40644  sge0xaddlem1  40650  sge0xadd  40652  sge0gtfsumgt  40660  nnfoctbdjlem  40672  iundjiun  40677  meadjun  40679  ismeannd  40684  voliunsge0lem  40689  caragenfiiuncl  40729  omeiunltfirp  40733  carageniuncl  40737  caragenunicl  40738  isomenndlem  40744  isomennd  40745  hoicvr  40762  ovnssle  40775  ovn0  40780  ovnsubadd  40786  hsphoidmvle2  40799  hoidmvval0b  40804  hoidmv1lelem1  40805  hoidmv1lelem2  40806  hoidmv1le  40808  hoidmvlelem2  40810  hoidmvlelem3  40811  hoidmvlelem5  40813  hoidmvle  40814  ovnhoilem1  40815  ovnhoi  40817  ovnlecvr2  40824  hspdifhsp  40830  hoidifhspdmvle  40834  hoiqssbl  40839  hspmbllem1  40840  hspmbllem2  40841  hspmbl  40843  hoimbl  40845  volico2  40855  ovolval2lem  40857  ovnsubadd2lem  40859  ovolval4lem1  40863  ovolval4lem2  40864  ovolval5lem1  40866  vonhoire  40886  iunhoiioo  40890  vonioo  40896  vonicc  40899  vonsn  40905  pimrecltpos  40919  incsmflem  40950  smfpimltxr  40956  smfconst  40958  decsmflem  40974  smfpimgtxr  40988  smfrec  40996  sharhght  41054