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

Theorem pm2.61dan 789
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 434 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
3 pm2.61dan.2 . . 3  |-  ( (
ph  /\  -.  ps )  ->  ch )
43ex 434 . 2  |-  ( ph  ->  ( -.  ps  ->  ch ) )
52, 4pm2.61d 158 1  |-  ( ph  ->  ch )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 369
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 185  df-an 371
This theorem is referenced by:  pm2.61ddan  790  pm2.61dda  791  nfsb4t  2080  ifeq1da  3814  ifeq2da  3815  ifclda  3816  ifeqda  3817  ifbothda  3819  2if2  3832  posn  4902  frsn  4904  somin1  5229  somincom  5230  xpcan  5269  fvmpti  5768  fvmptss  5777  funressn  5890  ovima0  6237  oeoa  7028  oeoe  7030  omabs  7078  eceqoveq  7197  domdifsn  7386  pw2f1olem  7407  mapdom1  7468  marypha1lem  7675  supval2  7697  infdifsn  7854  carden2b  8129  fidomtri  8155  dfac12lem2  8305  cdadom1  8347  infunsdom1  8374  infunsdom  8375  itunisuc  8580  gchdomtri  8788  xrmax2  11140  xrmin1  11141  ifle  11159  xmulneg1  11224  xrsupsslem  11261  xrinfmsslem  11262  fzneuz  11533  seqf1olem1  11837  bccmpl  12077  bcval5  12086  bcpasc  12089  bccl  12090  hasheni  12111  hashfn  12130  hashdom  12134  hashdomi  12135  hashge1  12144  hashbc  12198  sumz  13191  sumss  13193  sumsplit  13227  bitsmod  13624  sadadd2lem2  13638  sadcaddlem  13645  gcddvds  13691  gcdcl  13693  gcdneg  13702  pcgcd  13936  pcmpt  13946  pcmpt2  13947  pcprod  13949  fldivp1  13951  prmreclem4  13972  vdwlem6  14039  ramub1lem1  14079  cidpropd  14641  rescabs  14738  lubval  15146  glbval  15159  joinval  15167  meetval  15181  acsexdimd  15345  gsumpropd2lem  15496  gsumval2  15504  f1otrspeq  15944  pmtrfinv  15958  psgnunilem1  15990  gsumval3OLD  16373  gsumval3  16376  ablfac1c  16562  ablfac1eu  16564  mgpress  16592  psrbas  17428  psrbasOLD  17429  resspsrbas  17467  mplmonmul  17523  mplcoe1  17524  mplcoe5  17528  mplcoe2OLD  17530  opsrle  17537  opsrbaslem  17539  psrbaspropd  17669  mplbaspropd  17671  frlmsslsp  18203  frlmsslspOLD  18204  mdet1  18388  mdetunilem7  18404  mdetunilem9  18406  maducoeval2  18426  madurid  18430  opnnei  18704  restbas  18742  hauspwdom  19085  ptcmplem5  19608  xrsmopn  20369  xrhmeo  20498  lebnum  20516  pcohtpylem  20571  pcoass  20576  pcorevlem  20578  icombl  21025  ioombl  21026  mbfconstlem  21087  mbfima  21090  i1fd  21139  mbfi1fseqlem5  21177  itg2const2  21199  itg2seq  21200  itg2uba  21201  itg2splitlem  21206  itg2split  21207  itg2monolem1  21208  itg2gt0  21218  itg2cnlem1  21219  itg2cnlem2  21220  iblss  21262  iblss2  21263  itgss  21269  bddmulibl  21296  coemullem  21697  aaliou2b  21787  isppw2  22433  mule1  22466  ppip1le  22479  dchrelbas3  22557  dchrpt  22586  bposlem3  22605  bposlem5  22607  bposlem6  22608  lgslem4  22618  lgsneg  22638  lgsmod  22640  lgsdilem  22641  lgsdir  22649  lgsdi  22651  lgsne0  22652  lgsquad3  22680  dchrvmasum2if  22726  midexlem  23063  nmcfnlbi  25424  elpreq  25868  disjdifprg  25887  xrge0npcan  26125  archiabl  26183  orngsqr  26240  esumcst  26483  hasheuni  26503  esumcvg  26504  ddemeas  26621  eulerpartlemgc  26714  eulerpartlemb  26720  plymulx  26918  signswmnd  26927  erdsze2lem1  27060  prod1  27426  prodss  27429  trpredlem1  27660  wl-cbvalnaed  28330  wl-nfeqfb  28335  itg2addnclem  28414  itg2addnclem2  28415  iblmulc2nc  28428  ftc1anclem5  28442  ftc1anc  28446  dvasin  28451  areacirclem5  28459  exmid2  28873  ttac  29356  pw2f1ocnv  29357  aomclem5  29382  isnumbasgrplem3  29432  iocmbl  29559  fnchoice  29722  fmul01lt1lem1  29736  fmul01lt1lem2  29737  stoweidlem14  29780  stoweidlem26  29792  stoweidlem28  29794  stoweidlem55  29821  stoweid  29829  stirlinglem5  29844  stirlinglem12  29851  sharhght  29872  mdetdiag  30867  3dim1  33004  3dim2  33005  3dim3  33006  3atlem3  33022  3atlem7  33026  lvolnle3at  33119  2lplnja  33156  paddasslem18  33374  lhpexle3lem  33548  4atex  33613  cdlemd5  33739  cdleme16  33822  cdleme20  33861  cdleme21j  33873  cdleme21  33874  cdleme32snaw  33972  cdleme32fvcl  33977  cdleme32le  33984  cdlemeg46gf  34070  cdleme48gfv  34074  cdleme50trn12  34089  cdlemg6  34160  cdlemg7N  34163  cdlemg38  34252  cdlemg46  34272  dibvalrel  34701  dihlss  34788  dihglblem5aN  34830  dihmeetbN  34841  dihmeetALTN  34865  dihatlat  34872  dihatexv  34876  dvh3dim2  34986  dvh3dim3N  34987  lclkrlem2h  35052  mapdh8d  35321  mapdh8g  35324  hdmap11lem2  35383
  Copyright terms: Public domain W3C validator