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 432 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
3 pm2.61dan.2 . . 3  |-  ( (
ph  /\  -.  ps )  ->  ch )
43ex 432 . 2  |-  ( ph  ->  ( -.  ps  ->  ch ) )
52, 4pm2.61d 158 1  |-  ( ph  ->  ch )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 367
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 369
This theorem is referenced by:  pm2.61ddan  790  pm2.61dda  791  nfsb4t  2144  ifeq1da  3900  ifeq2da  3901  ifclda  3902  ifeqda  3903  ifbothda  3905  2if2  3918  posn  4995  frsn  4997  somin1  5326  xpcan  5366  fvmpti  5869  fvmptss  5879  funressn  6000  ovima0  6371  oeoa  7182  oeoe  7184  omabs  7232  eceqoveq  7352  domdifsn  7537  pw2f1olem  7558  mapdom1  7619  marypha1lem  7826  supval2  7847  infdifsn  8005  carden2b  8279  fidomtri  8305  dfac12lem2  8455  cdadom1  8497  infunsdom1  8524  infunsdom  8525  itunisuc  8730  gchdomtri  8936  xrmax2  11316  xrmin1  11317  ifle  11335  xmulneg1  11400  xrsupsslem  11437  xrinfmsslem  11438  fzneuz  11699  seqf1olem1  12068  bccmpl  12308  bcval5  12317  bcpasc  12320  bccl  12321  hasheni  12342  hashfn  12365  hashdom  12369  hashdomi  12370  hashge1  12379  hashbc  12425  sumz  13565  sumss  13567  sumsplit  13604  prod1  13772  prodss  13775  bitsmod  14107  sadadd2lem2  14121  sadcaddlem  14128  gcddvds  14174  gcdcl  14176  gcdneg  14185  pcgcd  14422  pcmpt  14432  pcmpt2  14433  pcprod  14435  fldivp1  14437  prmreclem4  14458  vdwlem6  14525  ramub1lem1  14565  cidpropd  15135  rescabs  15258  lubval  15750  glbval  15763  joinval  15771  meetval  15785  acsexdimd  15949  gsumpropd2lem  16036  gsumval2  16043  f1otrspeq  16608  pmtrfinv  16622  psgnunilem1  16654  gsumval3OLD  17044  gsumval3  17047  ablfac1c  17254  ablfac1eu  17256  mgpress  17284  psrbas  18162  psrbasOLD  18163  resspsrbas  18202  mplmonmul  18258  mplcoe1  18259  mplcoe5  18263  mplcoe2OLD  18265  opsrle  18272  opsrbaslem  18274  psrbaspropd  18408  mplbaspropd  18410  frlmsslsp  18935  mdetdiag  19205  mdetunilem7  19224  mdetunilem9  19226  maducoeval2  19246  madurid  19250  opnnei  19726  restbas  19764  hauspwdom  20106  ptcmplem5  20660  xrsmopn  21421  xrhmeo  21550  lebnum  21568  pcohtpylem  21623  pcoass  21628  pcorevlem  21630  icombl  22078  ioombl  22079  mbfconstlem  22140  mbfima  22143  i1fd  22192  mbfi1fseqlem5  22230  itg2const2  22252  itg2seq  22253  itg2uba  22254  itg2splitlem  22259  itg2split  22260  itg2monolem1  22261  itg2gt0  22271  itg2cnlem1  22272  itg2cnlem2  22273  iblss  22315  iblss2  22316  itgss  22322  bddmulibl  22349  coemullem  22751  aaliou2b  22841  isppw2  23525  mule1  23558  ppip1le  23571  dchrelbas3  23649  dchrpt  23678  bposlem3  23697  bposlem5  23699  bposlem6  23700  lgslem4  23710  lgsneg  23730  lgsmod  23732  lgsdilem  23733  lgsdir  23741  lgsdi  23743  lgsne0  23744  lgsquad3  23772  dchrvmasum2if  23818  midexlem  24210  colperpex  24248  lnopp2hpgb  24273  lmieu  24291  nmcfnlbi  27108  elpreq  27565  disjdifprg  27594  disjun0  27614  xrge0npcan  27867  archiabl  27925  orngsqr  27979  esumcst  28242  esumrnmpt2  28247  hasheuni  28264  esumcvg  28265  ddemeas  28400  omssubadd  28463  eulerpartlemgc  28520  eulerpartlemb  28526  plymulx  28724  signswmnd  28733  signstfvneq0  28748  erdsze2lem1  28872  mrsubvrs  29107  trpredlem1  29511  wl-cbvalnaed  30186  wl-nfeqfb  30191  itg2addnclem  30268  itg2addnclem2  30269  iblmulc2nc  30282  ftc1anclem5  30296  ftc1anc  30300  dvasin  30305  areacirclem5  30313  exmid2  30701  ttac  31180  pw2f1ocnv  31181  aomclem5  31206  isnumbasgrplem3  31258  iocmbl  31384  radcnvrat  31399  dvdslcm  31408  lcmcl  31411  lcmneg  31413  lcmgcd  31417  bccbc  31454  binomcxp  31466  fnchoice  31607  fzisoeu  31701  fperiodmul  31705  upbdrech2  31709  fzdifsuc2  31713  ioondisj2  31726  iccdifprioo  31757  fsumsplitsn  31772  fmul01lt1lem1  31779  fmul01lt1lem2  31780  fprodsplitsn  31793  fprodle  31805  limciccioolb  31828  lptioo2  31838  lptioo1  31839  limcicciooub  31844  lptre2pt  31847  limcresiooub  31849  limcresioolb  31850  limcleqr  31851  coskpi2  31867  cosknegpi  31870  icccncfext  31891  cncfiooicclem1  31897  cncfiooicc  31898  cncfiooiccre  31899  dvbdfbdioolem2  31927  ioodvbdlimc1lem1  31929  ioodvbdlimc1lem2  31930  ioodvbdlimc2lem  31932  dvnxpaek  31940  dvnprodlem1  31944  dvnprodlem3  31946  volioc  31972  itgioocnicc  31977  iblcncfioo  31978  stoweidlem14  31997  stoweidlem26  32009  stoweidlem28  32011  stoweidlem55  32038  stoweid  32046  stirlinglem5  32061  stirlinglem12  32068  dirkerper  32079  dirkertrigeqlem3  32083  dirkertrigeq  32084  dirkercncflem1  32086  dirkercncflem2  32087  dirkercncf  32090  fourierdlem10  32100  fourierdlem12  32102  fourierdlem24  32114  fourierdlem30  32120  fourierdlem31  32121  fourierdlem32  32122  fourierdlem33  32123  fourierdlem34  32124  fourierdlem35  32125  fourierdlem37  32127  fourierdlem40  32130  fourierdlem41  32131  fourierdlem42  32132  fourierdlem43  32133  fourierdlem44  32134  fourierdlem46  32136  fourierdlem48  32138  fourierdlem49  32139  fourierdlem51  32141  fourierdlem54  32144  fourierdlem62  32152  fourierdlem64  32154  fourierdlem65  32155  fourierdlem70  32160  fourierdlem71  32161  fourierdlem73  32163  fourierdlem74  32164  fourierdlem75  32165  fourierdlem78  32168  fourierdlem79  32169  fourierdlem80  32170  fourierdlem81  32171  fourierdlem82  32172  fourierdlem92  32182  fourierdlem93  32183  fourierdlem97  32187  fourierdlem101  32191  fourierdlem102  32192  fourierdlem103  32193  fourierdlem104  32194  fourierdlem109  32199  fourierdlem114  32204  sqwvfoura  32212  sqwvfourb  32213  fourierswlem  32214  fouriersw  32215  elaa2lem  32217  etransclem15  32233  etransclem19  32237  etransclem20  32238  etransclem22  32240  etransclem23  32241  etransclem24  32242  etransclem25  32243  etransclem27  32245  etransclem28  32246  etransclem35  32253  etransclem38  32256  sharhght  32283  3dim1  35639  3dim2  35640  3dim3  35641  3atlem3  35657  3atlem7  35661  lvolnle3at  35754  2lplnja  35791  paddasslem18  36009  lhpexle3lem  36183  4atex  36248  cdlemd5  36375  cdleme16  36458  cdleme20  36498  cdleme21j  36510  cdleme21  36511  cdleme32snaw  36609  cdleme32fvcl  36614  cdleme32le  36621  cdlemeg46gf  36707  cdleme48gfv  36711  cdleme50trn12  36726  cdlemg6  36797  cdlemg7N  36800  cdlemg38  36889  cdlemg46  36909  dibvalrel  37338  dihlss  37425  dihglblem5aN  37467  dihmeetbN  37478  dihmeetALTN  37502  dihatlat  37509  dihatexv  37513  dvh3dim2  37623  dvh3dim3N  37624  lclkrlem2h  37689  mapdh8d  37958  mapdh8g  37961  hdmap11lem2  38020
  Copyright terms: Public domain W3C validator