MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm2.61dan Structured version   Unicode version

Theorem pm2.61dan 798
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
StepHypRef Expression
1 pm2.61dan.1 . . 3  |-  ( (
ph  /\  ps )  ->  ch )
21ex 435 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
3 pm2.61dan.2 . . 3  |-  ( (
ph  /\  -.  ps )  ->  ch )
43ex 435 . 2  |-  ( ph  ->  ( -.  ps  ->  ch ) )
52, 4pm2.61d 161 1  |-  ( ph  ->  ch )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 370
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 188  df-an 372
This theorem is referenced by:  pm2.61ddan  799  pm2.61dda  800  nfsb4t  2189  ifeq1da  3879  ifeq2da  3880  ifclda  3881  ifeqda  3882  ifbothda  3884  2if2  3897  nelsn  3968  posn  4860  frsn  4862  somin1  5190  xpcan  5230  fvmpti  5902  fvmptss  5913  funressn  6031  ovima0  6401  oeoa  7248  oeoe  7250  omabs  7298  eceqoveq  7418  domdifsn  7603  pw2f1olem  7624  mapdom1  7685  marypha1lem  7895  supval2  7917  infdifsn  8109  carden2b  8348  fidomtri  8374  dfac12lem2  8520  cdadom1  8562  infunsdom1  8589  infunsdom  8590  itunisuc  8795  gchdomtri  9000  xrmax2  11417  xrmin1  11418  ifle  11436  xmulneg1  11501  xrsupsslem  11538  xrinfmsslem  11539  fzneuz  11821  seqf1olem1  12197  bccmpl  12439  bcval5  12448  bcpasc  12451  bccl  12452  hasheni  12476  hashfn  12499  hashdom  12503  hashdomi  12504  hashge1  12513  hashbc  12559  sumz  13726  sumss  13728  sumsplit  13767  prod1  13936  prodss  13939  fprodsplitsn  13981  fprodle  13988  bitsmod  14348  sadadd2lem2  14362  sadcaddlem  14369  gcddvds  14415  gcdcl  14418  gcdneg  14428  dvdslcm  14501  lcmcl  14504  lcmneg  14506  lcmgcd  14510  lcmfcl  14539  dvdslcmf  14542  pcgcd  14765  pcmpt  14775  pcmpt2  14776  pcprod  14778  fldivp1  14780  prmreclem4  14801  vdwlem6  14874  ramub1lem1  14922  cidpropd  15553  rescabs  15676  lubval  16168  glbval  16181  joinval  16189  meetval  16203  acsexdimd  16367  gsumpropd2lem  16454  gsumval2  16461  f1otrspeq  17026  pmtrfinv  17040  psgnunilem1  17072  gsumval3  17479  ablfac1c  17642  ablfac1eu  17644  mgpress  17672  psrbas  18540  resspsrbas  18577  mplmonmul  18626  mplcoe1  18627  mplcoe5  18630  opsrle  18637  opsrbaslem  18639  psrbaspropd  18766  mplbaspropd  18768  frlmsslsp  19291  mdetdiag  19561  mdetunilem7  19580  mdetunilem9  19582  maducoeval2  19602  madurid  19606  opnnei  20073  restbas  20111  hauspwdom  20453  ptcmplem5  21008  xrsmopn  21767  xrhmeo  21911  lebnum  21932  pcohtpylem  21987  pcoass  21992  pcorevlem  21994  icombl  22454  ioombl  22455  mbfconstlem  22522  mbfima  22525  i1fd  22576  mbfi1fseqlem5  22614  itg2const2  22636  itg2seq  22637  itg2uba  22638  itg2splitlem  22643  itg2split  22644  itg2monolem1  22645  itg2gt0  22655  itg2cnlem1  22656  itg2cnlem2  22657  iblss  22699  iblss2  22700  itgss  22706  bddmulibl  22733  coemullem  23141  aaliou2b  23234  isppw2  23979  mule1  24012  ppip1le  24025  dchrelbas3  24103  dchrpt  24132  bposlem3  24151  bposlem5  24153  bposlem6  24154  lgslem4  24164  lgsneg  24184  lgsmod  24186  lgsdilem  24187  lgsdir  24195  lgsdi  24197  lgsne0  24198  lgsquad3  24226  dchrvmasum2if  24272  midexlem  24674  colperpex  24712  outpasch  24734  hlpasch  24735  lnopp2hpgb  24742  lmieu  24763  inaghl  24818  cgrg3col4  24821  nmcfnlbi  27642  elpreq  28097  disjdifprg  28126  disjun0  28146  f1ocnt  28321  xrge0npcan  28403  archiabl  28461  orngsqr  28514  psgnfzto1stlem  28560  1smat1  28577  esumcst  28831  esumrnmpt2  28836  hasheuni  28853  esumcvg  28854  ddemeas  29006  omssubadd  29075  omssubaddOLD  29079  eulerpartlemgc  29142  eulerpartlemb  29148  plymulx  29384  signswmnd  29393  signstfvneq0  29408  erdsze2lem1  29873  mrsubvrs  30107  trpredlem1  30414  wl-cbvalnaed  31772  wl-nfeqfb  31777  poimirlem15  31862  poimirlem22  31869  itg2addnclem  31900  itg2addnclem2  31901  iblmulc2nc  31914  ftc1anclem5  31928  ftc1anc  31932  dvasin  31935  areacirclem5  31943  exmid2  32242  3dim1  32944  3dim2  32945  3dim3  32946  3atlem3  32962  3atlem7  32966  lvolnle3at  33059  2lplnja  33096  paddasslem18  33314  lhpexle3lem  33488  4atex  33553  cdlemd5  33680  cdleme16  33763  cdleme20  33803  cdleme21j  33815  cdleme21  33816  cdleme32snaw  33914  cdleme32fvcl  33919  cdleme32le  33926  cdlemeg46gf  34012  cdleme48gfv  34016  cdleme50trn12  34031  cdlemg6  34102  cdlemg7N  34105  cdlemg38  34194  cdlemg46  34214  dibvalrel  34643  dihlss  34730  dihglblem5aN  34772  dihmeetbN  34783  dihmeetALTN  34807  dihatlat  34814  dihatexv  34818  dvh3dim2  34928  dvh3dim3N  34929  lclkrlem2h  34994  mapdh8d  35263  mapdh8g  35266  hdmap11lem2  35325  ttac  35804  pw2f1ocnv  35805  aomclem5  35829  isnumbasgrplem3  35877  iocmbl  36010  radcnvrat  36576  bccbc  36607  binomcxp  36619  fnchoice  37266  fiiuncl  37322  disjxp1  37327  founiiun0  37369  fzisoeu  37415  fperiodmul  37419  upbdrech2  37423  fzdifsuc2  37427  uzfissfz  37446  supxrgere  37453  supxrgelem  37457  supxrge  37458  suplesup  37459  infrpge  37471  xrlexaddrp  37472  xralrple2  37474  ioondisj2  37481  iccdifprioo  37509  fsumsplitsn  37533  fmul01lt1lem1  37545  fmul01lt1lem2  37546  limciccioolb  37584  lptioo2  37594  lptioo1  37595  limcicciooub  37600  lptre2pt  37603  limcresiooub  37606  limcresioolb  37607  limcleqr  37608  coskpi2  37624  cosknegpi  37627  icccncfext  37648  cncfiooicclem1  37654  cncfiooicc  37655  cncfiooiccre  37656  dvbdfbdioolem2  37684  ioodvbdlimc1lem1  37686  ioodvbdlimc1lem2  37687  ioodvbdlimc1lem1OLD  37688  ioodvbdlimc1lem2OLD  37689  ioodvbdlimc2lem  37691  ioodvbdlimc2lemOLD  37692  dvnxpaek  37700  dvnprodlem1  37704  dvnprodlem3  37706  volioc  37732  itgioocnicc  37737  iblcncfioo  37738  stoweidlem14  37757  stoweidlem26  37769  stoweidlem28  37771  stoweidlem55  37799  stoweid  37808  stirlinglem5  37823  stirlinglem12  37830  dirkerper  37841  dirkertrigeqlem3  37845  dirkertrigeq  37846  dirkercncflem1  37848  dirkercncflem2  37849  dirkercncf  37852  fourierdlem10  37862  fourierdlem12  37864  fourierdlem24  37876  fourierdlem30  37882  fourierdlem31  37883  fourierdlem31OLD  37884  fourierdlem32  37885  fourierdlem33  37886  fourierdlem34  37887  fourierdlem35  37888  fourierdlem37  37890  fourierdlem40  37893  fourierdlem41  37894  fourierdlem42  37895  fourierdlem42OLD  37896  fourierdlem43  37897  fourierdlem44  37898  fourierdlem46  37899  fourierdlem48  37901  fourierdlem49  37902  fourierdlem51  37904  fourierdlem54  37907  fourierdlem62  37915  fourierdlem64  37917  fourierdlem65  37918  fourierdlem70  37923  fourierdlem71  37924  fourierdlem73  37926  fourierdlem74  37927  fourierdlem75  37928  fourierdlem78  37931  fourierdlem79  37932  fourierdlem80  37933  fourierdlem81  37934  fourierdlem82  37935  fourierdlem92  37945  fourierdlem93  37946  fourierdlem97  37950  fourierdlem101  37954  fourierdlem102  37955  fourierdlem103  37956  fourierdlem104  37957  fourierdlem109  37962  fourierdlem114  37967  sqwvfoura  37975  sqwvfourb  37976  fourierswlem  37977  fouriersw  37978  elaa2lem  37980  elaa2lemOLD  37981  etransclem15  37997  etransclem19  38001  etransclem20  38002  etransclem22  38004  etransclem23  38005  etransclem24  38006  etransclem25  38007  etransclem27  38009  etransclem28  38010  etransclem35  38017  etransclem38  38020  prsal  38043  sge0sn  38072  sge0tsms  38073  sge0cl  38074  sge0f1o  38075  sge0sup  38084  sge0less  38085  sge0pr  38087  sge0prle  38094  sge0le  38100  sge0split  38102  sge0splitmpt  38104  sge0iunmptlemfi  38106  sge0iunmpt  38111  sge0isum  38120  sge0xaddlem1  38126  sge0xadd  38128  sge0gtfsumgt  38136  nnfoctbdjlem  38144  iundjiun  38149  meadjun  38151  ismeannd  38156  caragenfiiuncl  38187  omeiunltfirp  38191  carageniuncl  38195  caragenunicl  38196  isomenndlem  38202  isomennd  38203  volico  38210  hoicvr  38217  ovnssle  38230  ovn0  38235  ovnsubadd  38241  hsphoidmvle2  38254  hoidmvval0b  38259  hoidmv1lelem1  38260  hoidmv1lelem2  38261  hoidmv1le  38263  hoidmvlelem2  38265  hoidmvlelem3  38266  hoidmvlelem5  38268  hoidmvle  38269  ovnhoilem1  38270  ovnhoi  38272  sharhght  38288
  Copyright terms: Public domain W3C validator