Theorem pm2.61dan 767

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 424	. 2 |- ( ph -> ( ps -> ch ) )
3		pm2.61dan.2	. . 3 |- ( ( ph /\ -. ps ) -> ch )
4	3	ex 424	. 2 |- ( ph -> ( -. ps -> ch ) )
5	2, 4	pm2.61d 152	1 |- ( ph -> ch )

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

This theorem is referenced by:  pm2.61ddan  768  pm2.61dda  769  ifeq1da  3728  ifeq2da  3729  ifclda  3730  ifbothda  3733  posn  4909  frsn  4911  somin1  5233  somincom  5234  xpcan  5268  fvmpti  5768  fvmptss  5776  funressn  5882  riotassuni  6551  oeoa  6803  oeoe  6805  omabs  6853  eceqoveq  6972  domdifsn  7154  pw2f1olem  7175  mapdom1  7235  marypha1lem  7400  infdifsn  7571  carden2b  7814  fidomtri  7840  dfac12lem2  7984  cdadom1  8026  infunsdom1  8053  infunsdom  8054  itunisuc  8259  gchdomtri  8464  xrmax2  10724  xrmin1  10725  ifle  10743  xmulneg1  10808  xrsupsslem  10845  xrinfmsslem  10846  fzneuz  11087  seqf1olem1  11321  bccmpl  11559  bcval5  11568  bcpasc  11571  bccl  11572  hasheni  11591  hashfn  11608  hashdom  11612  hashdomi  11613  hashge1  11622  hashbc  11661  sumz  12475  sumss  12477  sumsplit  12511  bitsmod  12907  sadadd2lem2  12921  sadcaddlem  12928  gcddvds  12974  gcdcl  12976  gcdneg  12985  pcgcd  13210  pcmpt  13220  pcmpt2  13221  pcprod  13223  fldivp1  13225  prmreclem4  13246  vdwlem6  13313  ramub1lem1  13353  cidpropd  13895  rescabs  13992  acsexdimd  14568  gsumval2  14742  gsumval3  15473  ablfac1c  15588  ablfac1eu  15590  mgpress  15618  psrbas  16402  resspsrbas  16437  mplmonmul  16486  mplcoe1  16487  mplcoe2  16489  opsrle  16495  opsrbaslem  16497  psrbaspropd  16587  mplbaspropd  16589  opnnei  17143  restbas  17180  hauspwdom  17521  ptcmplem5  18044  xrsmopn  18800  xrhmeo  18928  lebnum  18946  pcohtpylem  19001  pcoass  19006  pcorevlem  19008  icombl  19415  ioombl  19416  mbfconstlem  19478  mbfima  19481  i1fd  19530  mbfi1fseqlem5  19568  itg2const2  19590  itg2seq  19591  itg2uba  19592  itg2splitlem  19597  itg2split  19598  itg2monolem1  19599  itg2gt0  19609  itg2cnlem1  19610  itg2cnlem2  19611  iblss  19653  iblss2  19654  itgss  19660  bddmulibl  19687  coemullem  20125  aaliou2b  20215  isppw2  20855  mule1  20888  ppip1le  20901  dchrelbas3  20979  dchrpt  21008  bposlem3  21027  bposlem5  21029  bposlem6  21030  lgslem4  21040  lgsneg  21060  lgsmod  21062  lgsdilem  21063  lgsdir  21071  lgsdi  21073  lgsne0  21074  lgsquad3  21102  dchrvmasum2if  21148  nmcfnlbi  23512  elpreq  23956  disjdifprg  23974  xrge0npcan  24173  gsumpropd2lem  24177  ofldsqr  24197  esumcst  24412  hasheuni  24432  esumcvg  24433  erdsze2lem1  24846  prod1  25227  prodss  25230  trpredlem1  25448  itg2addnclem  26159  itg2addnclem2  26160  iblmulc2nc  26173  areacirclem6  26190  ttac  27001  pw2f1ocnv  27002  aomclem5  27027  frlmsslsp  27120  isnumbasgrplem3  27142  f1otrspeq  27262  pmtrfinv  27274  psgnunilem1  27288  fnchoice  27571  fmul01lt1lem1  27585  fmul01lt1lem2  27586  stoweidlem14  27634  stoweidlem26  27646  stoweidlem28  27648  stoweidlem55  27675  stoweid  27683  stirlinglem5  27698  stirlinglem12  27705  sharhght  27726  2if2  27945  3dim1  29953  3dim2  29954  3dim3  29955  3atlem3  29971  3atlem7  29975  lvolnle3at  30068  2lplnja  30105  paddasslem18  30323  lhpexle3lem  30497  4atex  30562  cdlemd5  30688  cdleme16  30771  cdleme20  30810  cdleme21j  30822  cdleme21  30823  cdleme32snaw  30921  cdleme32fvcl  30926  cdleme32le  30933  cdlemeg46gf  31019  cdleme48gfv  31023  cdleme50trn12  31038  cdlemg6  31109  cdlemg7N  31112  cdlemg38  31201  cdlemg46  31221  dibvalrel  31650  dihlss  31737  dihglblem5aN  31779  dihmeetbN  31790  dihmeetALTN  31814  dihatlat  31821  dihatexv  31825  dvh3dim2  31935  dvh3dim3N  31936  lclkrlem2h  32001  mapdh8d  32270  mapdh8g  32273  hdmap11lem2  32332

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

This theorem depends on definitions:  df-bi 178  df-an 361