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  2184  ifeq1da  3945  ifeq2da  3946  ifclda  3947  ifeqda  3948  ifbothda  3950  2if2  3963  posn  4923  frsn  4925  somin1  5253  xpcan  5293  fvmpti  5963  fvmptss  5974  funressn  6092  ovima0  6462  oeoa  7306  oeoe  7308  omabs  7356  eceqoveq  7476  domdifsn  7661  pw2f1olem  7682  mapdom1  7743  marypha1lem  7953  supval2  7975  infdifsn  8161  carden2b  8400  fidomtri  8426  dfac12lem2  8572  cdadom1  8614  infunsdom1  8641  infunsdom  8642  itunisuc  8847  gchdomtri  9053  xrmax2  11471  xrmin1  11472  ifle  11490  xmulneg1  11555  xrsupsslem  11592  xrinfmsslem  11593  fzneuz  11873  seqf1olem1  12249  bccmpl  12491  bcval5  12500  bcpasc  12503  bccl  12504  hasheni  12528  hashfn  12551  hashdom  12555  hashdomi  12556  hashge1  12565  hashbc  12611  sumz  13766  sumss  13768  sumsplit  13807  prod1  13976  prodss  13979  fprodsplitsn  14021  fprodle  14028  bitsmod  14384  sadadd2lem2  14398  sadcaddlem  14405  gcddvds  14451  gcdcl  14454  gcdneg  14464  dvdslcm  14534  lcmcl  14537  lcmneg  14539  lcmgcd  14543  lcmfcl  14572  dvdslcmf  14575  pcgcd  14790  pcmpt  14800  pcmpt2  14801  pcprod  14803  fldivp1  14805  prmreclem4  14826  vdwlem6  14899  ramub1lem1  14947  cidpropd  15566  rescabs  15689  lubval  16181  glbval  16194  joinval  16202  meetval  16216  acsexdimd  16380  gsumpropd2lem  16467  gsumval2  16474  f1otrspeq  17039  pmtrfinv  17053  psgnunilem1  17085  gsumval3  17476  ablfac1c  17639  ablfac1eu  17641  mgpress  17669  psrbas  18537  resspsrbas  18574  mplmonmul  18623  mplcoe1  18624  mplcoe5  18627  opsrle  18634  opsrbaslem  18636  psrbaspropd  18763  mplbaspropd  18765  frlmsslsp  19285  mdetdiag  19555  mdetunilem7  19574  mdetunilem9  19576  maducoeval2  19596  madurid  19600  opnnei  20067  restbas  20105  hauspwdom  20447  ptcmplem5  21002  xrsmopn  21741  xrhmeo  21870  lebnum  21888  pcohtpylem  21943  pcoass  21948  pcorevlem  21950  icombl  22394  ioombl  22395  mbfconstlem  22462  mbfima  22465  i1fd  22516  mbfi1fseqlem5  22554  itg2const2  22576  itg2seq  22577  itg2uba  22578  itg2splitlem  22583  itg2split  22584  itg2monolem1  22585  itg2gt0  22595  itg2cnlem1  22596  itg2cnlem2  22597  iblss  22639  iblss2  22640  itgss  22646  bddmulibl  22673  coemullem  23072  aaliou2b  23162  isppw2  23905  mule1  23938  ppip1le  23951  dchrelbas3  24029  dchrpt  24058  bposlem3  24077  bposlem5  24079  bposlem6  24080  lgslem4  24090  lgsneg  24110  lgsmod  24112  lgsdilem  24113  lgsdir  24121  lgsdi  24123  lgsne0  24124  lgsquad3  24152  dchrvmasum2if  24198  midexlem  24594  colperpex  24632  outpasch  24654  lnopp2hpgb  24661  lmieu  24682  nmcfnlbi  27540  elpreq  27995  disjdifprg  28024  disjun0  28044  f1ocnt  28212  xrge0npcan  28295  archiabl  28353  orngsqr  28406  psgnfzto1stlem  28452  1smat1  28469  esumcst  28723  esumrnmpt2  28728  hasheuni  28745  esumcvg  28746  ddemeas  28898  omssubadd  28961  eulerpartlemgc  29021  eulerpartlemb  29027  plymulx  29225  signswmnd  29234  signstfvneq0  29249  erdsze2lem1  29714  mrsubvrs  29948  trpredlem1  30255  wl-cbvalnaed  31572  wl-nfeqfb  31577  poimirlem15  31659  poimirlem22  31666  itg2addnclem  31697  itg2addnclem2  31698  iblmulc2nc  31711  ftc1anclem5  31725  ftc1anc  31729  dvasin  31732  areacirclem5  31740  exmid2  32039  3dim1  32741  3dim2  32742  3dim3  32743  3atlem3  32759  3atlem7  32763  lvolnle3at  32856  2lplnja  32893  paddasslem18  33111  lhpexle3lem  33285  4atex  33350  cdlemd5  33477  cdleme16  33560  cdleme20  33600  cdleme21j  33612  cdleme21  33613  cdleme32snaw  33711  cdleme32fvcl  33716  cdleme32le  33723  cdlemeg46gf  33809  cdleme48gfv  33813  cdleme50trn12  33828  cdlemg6  33899  cdlemg7N  33902  cdlemg38  33991  cdlemg46  34011  dibvalrel  34440  dihlss  34527  dihglblem5aN  34569  dihmeetbN  34580  dihmeetALTN  34604  dihatlat  34611  dihatexv  34615  dvh3dim2  34725  dvh3dim3N  34726  lclkrlem2h  34791  mapdh8d  35060  mapdh8g  35063  hdmap11lem2  35122  ttac  35597  pw2f1ocnv  35598  aomclem5  35622  isnumbasgrplem3  35670  iocmbl  35796  radcnvrat  36300  bccbc  36331  binomcxp  36343  fnchoice  36990  nelsn  37042  fiiuncl  37048  founiiun0  37088  fzisoeu  37127  fperiodmul  37131  upbdrech2  37135  fzdifsuc2  37139  uzfissfz  37158  supxrgere  37165  supxrgelem  37169  supxrge  37170  suplesup  37171  ioondisj2  37174  iccdifprioo  37202  fsumsplitsn  37224  fmul01lt1lem1  37234  fmul01lt1lem2  37235  limciccioolb  37273  lptioo2  37283  lptioo1  37284  limcicciooub  37289  lptre2pt  37292  limcresiooub  37295  limcresioolb  37296  limcleqr  37297  coskpi2  37313  cosknegpi  37316  icccncfext  37337  cncfiooicclem1  37343  cncfiooicc  37344  cncfiooiccre  37345  dvbdfbdioolem2  37373  ioodvbdlimc1lem1  37375  ioodvbdlimc1lem2  37376  ioodvbdlimc2lem  37378  dvnxpaek  37386  dvnprodlem1  37390  dvnprodlem3  37392  volioc  37418  itgioocnicc  37423  iblcncfioo  37424  stoweidlem14  37443  stoweidlem26  37455  stoweidlem28  37457  stoweidlem55  37485  stoweid  37494  stirlinglem5  37509  stirlinglem12  37516  dirkerper  37527  dirkertrigeqlem3  37531  dirkertrigeq  37532  dirkercncflem1  37534  dirkercncflem2  37535  dirkercncf  37538  fourierdlem10  37548  fourierdlem12  37550  fourierdlem24  37562  fourierdlem30  37568  fourierdlem31  37569  fourierdlem32  37570  fourierdlem33  37571  fourierdlem34  37572  fourierdlem35  37573  fourierdlem37  37575  fourierdlem40  37578  fourierdlem41  37579  fourierdlem42  37580  fourierdlem43  37581  fourierdlem44  37582  fourierdlem46  37584  fourierdlem48  37586  fourierdlem49  37587  fourierdlem51  37589  fourierdlem54  37592  fourierdlem62  37600  fourierdlem64  37602  fourierdlem65  37603  fourierdlem70  37608  fourierdlem71  37609  fourierdlem73  37611  fourierdlem74  37612  fourierdlem75  37613  fourierdlem78  37616  fourierdlem79  37617  fourierdlem80  37618  fourierdlem81  37619  fourierdlem82  37620  fourierdlem92  37630  fourierdlem93  37631  fourierdlem97  37635  fourierdlem101  37639  fourierdlem102  37640  fourierdlem103  37641  fourierdlem104  37642  fourierdlem109  37647  fourierdlem114  37652  sqwvfoura  37660  sqwvfourb  37661  fourierswlem  37662  fouriersw  37663  elaa2lem  37665  etransclem15  37681  etransclem19  37685  etransclem20  37686  etransclem22  37688  etransclem23  37689  etransclem24  37690  etransclem25  37691  etransclem27  37693  etransclem28  37694  etransclem35  37701  etransclem38  37704  prsal  37726  sge0sn  37755  sge0tsms  37756  sge0cl  37757  sge0f1o  37758  sge0sup  37767  sge0less  37768  sge0pr  37770  sge0prle  37777  sge0le  37783  sge0split  37785  sge0splitmpt  37787  sge0iunmptlemfi  37789  sge0iunmpt  37794  nnfoctbdjlem  37802  iundjiun  37807  meadjun  37809  ismeannd  37814  caragenfiiuncl  37845  omeiunltfirp  37849  carageniuncl  37853  caragenunicl  37854  sharhght  37874
  Copyright terms: Public domain W3C validator