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

Theorem pm2.61dan 805
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 440 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
3 pm2.61dan.2 . . 3  |-  ( (
ph  /\  -.  ps )  ->  ch )
43ex 440 . 2  |-  ( ph  ->  ( -.  ps  ->  ch ) )
52, 4pm2.61d 163 1  |-  ( ph  ->  ch )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 375
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 190  df-an 377
This theorem is referenced by:  pm2.61ddan  806  pm2.61dda  807  ifpimpda  1451  nfsb4t  2228  ifeq1da  3922  ifeq2da  3923  ifclda  3924  ifeqda  3925  ifbothda  3927  2if2  3940  nelsn  4011  posn  4921  frsn  4923  somin1  5251  xpcan  5291  fvmpti  5969  fvmptss  5980  funressn  6100  ovima0  6474  oeoa  7323  oeoe  7325  omabs  7373  eceqoveq  7493  domdifsn  7680  pw2f1olem  7701  mapdom1  7762  marypha1lem  7972  supval2  7994  infdifsn  8187  carden2b  8426  fidomtri  8452  dfac12lem2  8599  cdadom1  8641  infunsdom1  8668  infunsdom  8669  itunisuc  8874  gchdomtri  9079  xrmax2  11499  xrmin1  11500  ifle  11518  xmulneg1  11583  xrsupsslem  11620  xrinfmsslem  11621  fzneuz  11903  seqf1olem1  12283  bccmpl  12525  bcval5  12534  bcpasc  12537  bccl  12538  hasheni  12562  hashfn  12585  hashdom  12589  hashdomi  12590  hashge1  12599  hashbc  12648  sumz  13836  sumss  13838  sumsplit  13877  prod1  14046  prodss  14049  fprodsplitsn  14091  fprodle  14098  bitsmod  14458  sadadd2lem2  14472  sadcaddlem  14479  gcddvds  14525  gcdcl  14528  gcdneg  14538  dvdslcm  14611  lcmcl  14614  lcmneg  14616  lcmgcd  14620  lcmfcl  14649  dvdslcmf  14652  pcgcd  14875  pcmpt  14885  pcmpt2  14886  pcprod  14888  fldivp1  14890  prmreclem4  14911  vdwlem6  14984  ramub1lem1  15032  cidpropd  15663  rescabs  15786  lubval  16278  glbval  16291  joinval  16299  meetval  16313  acsexdimd  16477  gsumpropd2lem  16564  gsumval2  16571  f1otrspeq  17136  pmtrfinv  17150  psgnunilem1  17182  gsumval3  17589  ablfac1c  17752  ablfac1eu  17754  mgpress  17782  psrbas  18650  resspsrbas  18687  mplmonmul  18736  mplcoe1  18737  mplcoe5  18740  opsrle  18747  opsrbaslem  18749  psrbaspropd  18876  mplbaspropd  18878  frlmsslsp  19402  mdetdiag  19672  mdetunilem7  19691  mdetunilem9  19693  maducoeval2  19713  madurid  19717  opnnei  20184  restbas  20222  hauspwdom  20564  ptcmplem5  21119  xrsmopn  21878  xrhmeo  22022  lebnum  22043  pcohtpylem  22098  pcoass  22103  pcorevlem  22105  icombl  22565  ioombl  22566  mbfconstlem  22633  mbfima  22636  i1fd  22687  mbfi1fseqlem5  22725  itg2const2  22747  itg2seq  22748  itg2uba  22749  itg2splitlem  22754  itg2split  22755  itg2monolem1  22756  itg2gt0  22766  itg2cnlem1  22767  itg2cnlem2  22768  iblss  22810  iblss2  22811  itgss  22817  bddmulibl  22844  coemullem  23252  aaliou2b  23345  isppw2  24090  mule1  24123  ppip1le  24136  dchrelbas3  24214  dchrpt  24243  bposlem3  24262  bposlem5  24264  bposlem6  24265  lgslem4  24275  lgsneg  24295  lgsmod  24297  lgsdilem  24298  lgsdir  24306  lgsdi  24308  lgsne0  24309  lgsquad3  24337  dchrvmasum2if  24383  midexlem  24785  colperpex  24823  outpasch  24845  hlpasch  24846  lnopp2hpgb  24853  lmieu  24874  inaghl  24929  cgrg3col4  24932  nmcfnlbi  27753  elpreq  28205  disjdifprg  28233  disjun0  28253  f1ocnt  28424  xrge0npcan  28505  archiabl  28563  orngsqr  28615  psgnfzto1stlem  28661  1smat1  28678  esumcst  28932  esumrnmpt2  28937  hasheuni  28954  esumcvg  28955  ddemeas  29107  omssubadd  29176  omssubaddOLD  29180  eulerpartlemgc  29243  eulerpartlemb  29249  plymulx  29485  signswmnd  29494  signstfvneq0  29509  erdsze2lem1  29974  mrsubvrs  30208  trpredlem1  30516  wl-cbvalnaed  31909  wl-nfeqfb  31914  poimirlem15  31999  poimirlem22  32006  itg2addnclem  32037  itg2addnclem2  32038  iblmulc2nc  32051  ftc1anclem5  32065  ftc1anc  32069  dvasin  32072  areacirclem5  32080  exmid2  32379  3dim1  33076  3dim2  33077  3dim3  33078  3atlem3  33094  3atlem7  33098  lvolnle3at  33191  2lplnja  33228  paddasslem18  33446  lhpexle3lem  33620  4atex  33685  cdlemd5  33812  cdleme16  33895  cdleme20  33935  cdleme21j  33947  cdleme21  33948  cdleme32snaw  34046  cdleme32fvcl  34051  cdleme32le  34058  cdlemeg46gf  34144  cdleme48gfv  34148  cdleme50trn12  34163  cdlemg6  34234  cdlemg7N  34237  cdlemg38  34326  cdlemg46  34346  dibvalrel  34775  dihlss  34862  dihglblem5aN  34904  dihmeetbN  34915  dihmeetALTN  34939  dihatlat  34946  dihatexv  34950  dvh3dim2  35060  dvh3dim3N  35061  lclkrlem2h  35126  mapdh8d  35395  mapdh8g  35398  hdmap11lem2  35457  ttac  35935  pw2f1ocnv  35936  aomclem5  35960  isnumbasgrplem3  36008  iocmbl  36141  radcnvrat  36706  bccbc  36737  binomcxp  36749  fnchoice  37389  fiiuncl  37443  disjxp1  37448  founiiun0  37502  fzisoeu  37555  fperiodmul  37559  upbdrech2  37563  fzdifsuc2  37567  uzfissfz  37586  supxrgere  37593  supxrgelem  37597  supxrge  37598  suplesup  37599  infrpge  37611  xrlexaddrp  37612  xralrple2  37614  ioondisj2  37626  iccdifprioo  37654  fsumsplitsn  37686  fmul01lt1lem1  37699  fmul01lt1lem2  37700  limciccioolb  37738  lptioo2  37748  lptioo1  37749  limcicciooub  37754  lptre2pt  37757  limcresiooub  37760  limcresioolb  37761  limcleqr  37762  coskpi2  37778  cosknegpi  37781  icccncfext  37802  cncfiooicclem1  37808  cncfiooicc  37809  cncfiooiccre  37810  dvbdfbdioolem2  37838  ioodvbdlimc1lem1  37840  ioodvbdlimc1lem2  37841  ioodvbdlimc1lem1OLD  37842  ioodvbdlimc1lem2OLD  37843  ioodvbdlimc2lem  37845  ioodvbdlimc2lemOLD  37846  dvnxpaek  37854  dvnprodlem1  37858  dvnprodlem3  37860  volioc  37886  itgioocnicc  37891  iblcncfioo  37892  stoweidlem14  37911  stoweidlem26  37923  stoweidlem28  37925  stoweidlem55  37953  stoweid  37962  stirlinglem5  37977  stirlinglem12  37984  dirkerper  37995  dirkertrigeqlem3  37999  dirkertrigeq  38000  dirkercncflem1  38002  dirkercncflem2  38003  dirkercncf  38006  fourierdlem10  38016  fourierdlem12  38018  fourierdlem24  38030  fourierdlem30  38036  fourierdlem31  38037  fourierdlem31OLD  38038  fourierdlem32  38039  fourierdlem33  38040  fourierdlem34  38041  fourierdlem35  38042  fourierdlem37  38044  fourierdlem40  38047  fourierdlem41  38048  fourierdlem42  38049  fourierdlem42OLD  38050  fourierdlem43  38051  fourierdlem44  38052  fourierdlem46  38053  fourierdlem48  38055  fourierdlem49  38056  fourierdlem51  38058  fourierdlem54  38061  fourierdlem62  38069  fourierdlem64  38071  fourierdlem65  38072  fourierdlem70  38077  fourierdlem71  38078  fourierdlem73  38080  fourierdlem74  38081  fourierdlem75  38082  fourierdlem78  38085  fourierdlem79  38086  fourierdlem80  38087  fourierdlem81  38088  fourierdlem82  38089  fourierdlem92  38099  fourierdlem93  38100  fourierdlem97  38104  fourierdlem101  38108  fourierdlem102  38109  fourierdlem103  38110  fourierdlem104  38111  fourierdlem109  38116  fourierdlem114  38121  sqwvfoura  38129  sqwvfourb  38130  fourierswlem  38131  fouriersw  38132  elaa2lem  38134  elaa2lemOLD  38135  etransclem15  38151  etransclem19  38155  etransclem20  38156  etransclem22  38158  etransclem23  38159  etransclem24  38160  etransclem25  38161  etransclem27  38163  etransclem28  38164  etransclem35  38171  etransclem38  38174  qndenserrnbl  38201  prsal  38216  salexct  38230  sge0sn  38258  sge0tsms  38259  sge0cl  38260  sge0f1o  38261  sge0sup  38270  sge0less  38271  sge0pr  38273  sge0prle  38280  sge0le  38286  sge0split  38288  sge0splitmpt  38290  sge0iunmptlemfi  38292  sge0iunmpt  38297  sge0isum  38306  sge0xaddlem1  38312  sge0xadd  38314  sge0gtfsumgt  38322  nnfoctbdjlem  38330  iundjiun  38335  meadjun  38337  ismeannd  38342  caragenfiiuncl  38373  omeiunltfirp  38377  carageniuncl  38381  caragenunicl  38382  isomenndlem  38388  isomennd  38389  volico  38400  hoicvr  38407  ovnssle  38420  ovn0  38425  ovnsubadd  38431  hsphoidmvle2  38444  hoidmvval0b  38449  hoidmv1lelem1  38450  hoidmv1lelem2  38451  hoidmv1le  38453  hoidmvlelem2  38455  hoidmvlelem3  38456  hoidmvlelem5  38458  hoidmvle  38459  ovnhoilem1  38460  ovnhoi  38462  ovnlecvr2  38469  hspdifhsp  38475  hoidifhspdmvle  38479  hoiqssbl  38484  hspmbllem1  38485  hspmbllem2  38486  hspmbl  38488  hoimbl  38490  sharhght  38511  pthdlem1  39791
  Copyright terms: Public domain W3C validator