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  2087  ifeq1da  3917  ifeq2da  3918  ifclda  3919  ifeqda  3920  ifbothda  3922  2if2  3935  posn  5005  frsn  5007  somin1  5332  somincom  5333  xpcan  5372  fvmpti  5872  fvmptss  5881  funressn  5994  ovima0  6342  oeoa  7136  oeoe  7138  omabs  7186  eceqoveq  7305  domdifsn  7494  pw2f1olem  7515  mapdom1  7576  marypha1lem  7784  supval2  7806  infdifsn  7963  carden2b  8238  fidomtri  8264  dfac12lem2  8414  cdadom1  8456  infunsdom1  8483  infunsdom  8484  itunisuc  8689  gchdomtri  8897  xrmax2  11249  xrmin1  11250  ifle  11268  xmulneg1  11333  xrsupsslem  11370  xrinfmsslem  11371  fzneuz  11642  seqf1olem1  11946  bccmpl  12186  bcval5  12195  bcpasc  12198  bccl  12199  hasheni  12220  hashfn  12240  hashdom  12244  hashdomi  12245  hashge1  12254  hashbc  12308  sumz  13301  sumss  13303  sumsplit  13337  bitsmod  13734  sadadd2lem2  13748  sadcaddlem  13755  gcddvds  13801  gcdcl  13803  gcdneg  13812  pcgcd  14046  pcmpt  14056  pcmpt2  14057  pcprod  14059  fldivp1  14061  prmreclem4  14082  vdwlem6  14149  ramub1lem1  14189  cidpropd  14751  rescabs  14848  lubval  15256  glbval  15269  joinval  15277  meetval  15291  acsexdimd  15455  gsumpropd2lem  15607  gsumval2  15615  f1otrspeq  16055  pmtrfinv  16069  psgnunilem1  16101  gsumval3OLD  16486  gsumval3  16489  ablfac1c  16677  ablfac1eu  16679  mgpress  16707  psrbas  17554  psrbasOLD  17555  resspsrbas  17594  mplmonmul  17650  mplcoe1  17651  mplcoe5  17655  mplcoe2OLD  17657  opsrle  17664  opsrbaslem  17666  psrbaspropd  17796  mplbaspropd  17798  frlmsslsp  18332  frlmsslspOLD  18333  mdetdiag  18521  mdetunilem7  18540  mdetunilem9  18542  maducoeval2  18562  madurid  18566  opnnei  18840  restbas  18878  hauspwdom  19221  ptcmplem5  19744  xrsmopn  20505  xrhmeo  20634  lebnum  20652  pcohtpylem  20707  pcoass  20712  pcorevlem  20714  icombl  21161  ioombl  21162  mbfconstlem  21223  mbfima  21226  i1fd  21275  mbfi1fseqlem5  21313  itg2const2  21335  itg2seq  21336  itg2uba  21337  itg2splitlem  21342  itg2split  21343  itg2monolem1  21344  itg2gt0  21354  itg2cnlem1  21355  itg2cnlem2  21356  iblss  21398  iblss2  21399  itgss  21405  bddmulibl  21432  coemullem  21833  aaliou2b  21923  isppw2  22569  mule1  22602  ppip1le  22615  dchrelbas3  22693  dchrpt  22722  bposlem3  22741  bposlem5  22743  bposlem6  22744  lgslem4  22754  lgsneg  22774  lgsmod  22776  lgsdilem  22777  lgsdir  22785  lgsdi  22787  lgsne0  22788  lgsquad3  22816  dchrvmasum2if  22862  midexlem  23212  colperp  23243  nmcfnlbi  25591  elpreq  26035  disjdifprg  26053  xrge0npcan  26291  archiabl  26349  orngsqr  26406  esumcst  26648  hasheuni  26668  esumcvg  26669  ddemeas  26786  eulerpartlemgc  26879  eulerpartlemb  26885  plymulx  27083  signswmnd  27092  erdsze2lem1  27225  prod1  27591  prodss  27594  trpredlem1  27825  wl-cbvalnaed  28499  wl-nfeqfb  28504  itg2addnclem  28581  itg2addnclem2  28582  iblmulc2nc  28595  ftc1anclem5  28609  ftc1anc  28613  dvasin  28618  areacirclem5  28626  exmid2  29040  ttac  29523  pw2f1ocnv  29524  aomclem5  29549  isnumbasgrplem3  29599  iocmbl  29726  fnchoice  29889  fmul01lt1lem1  29903  fmul01lt1lem2  29904  stoweidlem14  29947  stoweidlem26  29959  stoweidlem28  29961  stoweidlem55  29988  stoweid  29996  stirlinglem5  30011  stirlinglem12  30018  sharhght  30039  3dim1  33417  3dim2  33418  3dim3  33419  3atlem3  33435  3atlem7  33439  lvolnle3at  33532  2lplnja  33569  paddasslem18  33787  lhpexle3lem  33961  4atex  34026  cdlemd5  34152  cdleme16  34235  cdleme20  34274  cdleme21j  34286  cdleme21  34287  cdleme32snaw  34385  cdleme32fvcl  34390  cdleme32le  34397  cdlemeg46gf  34483  cdleme48gfv  34487  cdleme50trn12  34502  cdlemg6  34573  cdlemg7N  34576  cdlemg38  34665  cdlemg46  34685  dibvalrel  35114  dihlss  35201  dihglblem5aN  35243  dihmeetbN  35254  dihmeetALTN  35278  dihatlat  35285  dihatexv  35289  dvh3dim2  35399  dvh3dim3N  35400  lclkrlem2h  35465  mapdh8d  35734  mapdh8g  35737  hdmap11lem2  35796
  Copyright terms: Public domain W3C validator