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

Theorem pm2.61i 164
Description: Inference eliminating an antecedent. (Contributed by NM, 5-Apr-1994.) (Proof shortened by Wolf Lammen, 12-Sep-2013.)
Hypotheses
Ref Expression
pm2.61i.1
pm2.61i.2
Assertion
Ref Expression
pm2.61i

Proof of Theorem pm2.61i
StepHypRef Expression
1 id 22 . 2
2 pm2.61i.2 . . 3
3 pm2.61i.1 . . 3
42, 3ja 161 . 2
51, 4ax-mp 5 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4
This theorem is referenced by:  pm2.61ii  165  pm2.61nii  166  pm2.61iii  167  pm2.65i  173  pm5.21nii  353  pm5.18  356  biass  359  pm2.61ian  790  ecase3  941  4cases  949  elimh  956  pm4.42  960  3ecase  1333  ifpid  1390  ax6e  2002  exdistrf  2075  equvini  2087  dfsb2  2114  sbequi  2116  sbi1  2133  sbcom3  2153  sbco2  2158  sbco3  2160  sb9  2169  ax12vALT  2171  hbs1  2180  nfsb  2184  2ax6e  2194  sbal  2206  ax12  2234  equid1  2237  equid1ALT  2255  dvelimf-o  2259  ax12inda2ALT  2276  ax12inda2  2277  eujustALT  2285  pm2.61ine  2770  pm2.61neOLD  2773  rgen2aOLD  2885  ralcom2  3022  eueq2  3273  moeq3  3276  mo2icl  3278  sbc2or  3336  sbcimdv  3396  unineq  3747  csb0  3822  sbcel12  3823  sbcne12  3827  sbcel2  3831  csbidm  3846  csbun  3857  csbin  3860  ralidm  3933  ifsb  3954  ifid  3978  ifnot  3986  ifan  3987  ifor  3988  csbif  3991  elimhyp  4000  elimhyp2v  4001  elimhyp3v  4002  elimhyp4v  4003  elimdhyp  4005  keephyp2v  4007  keephyp3v  4008  rabsnif  4099  tppreqb  4171  ssunsn2  4189  dfopif  4214  csbuni  4277  sbcbr123  4503  sbcbr  4505  unisn2  4588  intabs  4613  class2set  4619  snexALT  4638  dtru  4643  dtruALT  4684  snex  4693  dtruALT2  4696  copsexg  4737  copsexgOLD  4738  otsndisj  4757  otiunsndisj  4758  csbopab  4784  dfid3  4801  nsuceq0  4963  ordsssuc2  4971  csbxp  5086  csbres  5281  csbima12  5359  soirri  5398  soirriOLD  5403  csbrn  5473  dmsnopss  5485  dmsnsnsn  5491  opswap  5500  unixpid  5547  iotassuni  5572  iotaex  5573  dfiota4  5584  csbiota  5585  dffv3  5867  fvrn0  5893  ndmfv  5895  fveqres  5905  csbfv12  5906  csbfv  5909  dffv2  5946  fvco4i  5951  fvmptss  5964  fvmptex  5966  fvmptss2  5975  f0cli  6042  fvunsn  6103  fconst5  6128  csbriota  6269  riotassuniOLD  6294  csbov123  6330  csbov  6331  0neqopab  6341  elimdelov  6378  ovif12  6381  ndmovcl  6460  ndmovord  6465  elovmpt3imp  6533  difsnexi  6608  ordsuc  6649  ordsucelsuc  6657  1stval  6802  2ndval  6803  1st2val  6826  2nd2val  6827  bropopvvv  6880  suppimacnv  6929  suppssdm  6931  ressuppss  6938  suppun  6939  extmptsuppeq  6943  funsssuppss  6945  fczsupp0  6948  suppss  6949  suppssov1  6951  suppss2  6953  suppssfv  6955  supp0cosupp0  6958  imacosupp  6959  mpt2xopynvov0  6965  mpt2xopoveqd  6968  pwuninel  7023  smofvon2  7046  om0x  7188  brdomg  7546  snfi  7616  sdomirr  7674  domunsn  7687  2pwuninel  7692  snnen2o  7726  suppeqfsuppbi  7863  fsuppun  7868  funsnfsupp  7873  fipwuni  7906  oicl  7975  oif  7976  wemapso2  8000  card2on  8001  en2lp  8051  tctr  8192  r1tr  8215  rankdmr1  8240  r1pw  8284  r1pwOLD  8285  rankuni  8302  scottex  8324  cardidm  8361  alephcard  8472  alephnbtwn  8473  cdacomen  8582  cfub  8650  cardcf  8653  cflecard  8654  cfle  8655  cflim2  8664  cfidm  8676  isf32lem9  8762  itunisuc  8820  itunitc1  8821  itunitc  8822  ituniiun  8823  axcc2lem  8837  alephreg  8978  pwcfsdom  8979  cfpwsdom  8980  axunndlem1  8991  axpownd  8999  tskmcl  9240  addcompi  9293  addasspi  9294  mulcompi  9295  mulasspi  9296  distrpi  9297  addnidpi  9300  nlt1pi  9305  addcompq  9349  addcomnq  9350  mulcompq  9351  mulcomnq  9352  adderpq  9355  mulerpq  9356  addassnq  9357  mulassnq  9358  distrnq  9360  genpass  9408  addcompr  9420  mulcompr  9422  distrpr  9427  ltexprlem7  9441  addcomsr  9485  addasssr  9486  mulcomsr  9487  mulasssr  9488  distrsr  9489  uzssz  11129  uzwo  11173  uzwoOLD  11174  nn01to3  11204  elixx3g  11571  iooid  11586  elfz2  11708  injresinjlem  11925  injresinj  11926  fleqceilz  11981  modifeq2int  12049  ltweuz  12072  fzofi  12084  fsuppmapnn0fiubex  12098  hashrabrsn  12440  hashrabsn01  12441  hashrabsn1  12442  elprchashprn2  12461  hashss  12474  hashsnlei  12478  hash1snb  12479  hashgt12el  12481  hashgt12el2  12482  hash2pwpr  12519  hashge2el2dif  12521  ccatsymb  12600  swrd00  12645  swrdnd  12657  swrd0  12658  swrdccatin1  12708  repswswrd  12756  0csh0  12764  cshwcl  12769  cshwidxmod  12774  repswcshw  12780  cshw1  12790  modfsummods  13607  gcdaddmlem  14166  pcmptcl  14410  cshwshash  14589  strfvss  14650  strfvi  14672  setsnid  14674  ressbas  14687  ressbasss  14689  resslem  14690  ress0  14691  ressress  14694  strle1  14728  0rest  14827  firest  14830  topnval  14832  xpsaddlem  14972  xpsvsca  14976  homffval  15086  comfffval  15093  oppchomfval  15109  oppcbas  15113  fullfunc  15275  fthfunc  15276  natfval  15315  fucbas  15329  fuchom  15330  arwval  15370  coafval  15391  xpcbas  15447  xpchomfval  15448  xpccofval  15451  lubfun  15610  glbfun  15623  oduval  15760  oduleval  15761  odumeet  15770  odujoin  15772  ipopos  15790  plusffval  15877  grpidval  15887  gsum0  15905  frmdplusg  16022  frmd0  16028  mgm2nsgrplem2  16037  mgm2nsgrplem3  16038  sgrp2rid2  16044  grpinvfval  16088  grpinvfvi  16091  grpsubfval  16092  mulgfval  16143  mulgfvi  16146  cntrval  16357  oppgval  16382  oppgplusfval  16383  symgbas  16405  symgplusg  16414  psgnfval  16525  odfval  16557  oppglsm  16662  efgval  16735  mgpval  17144  mgpplusg  17145  ringidval  17155  opprval  17273  opprmulfval  17274  dvdsrval  17294  invrfval  17322  dvrfval  17333  staffval  17496  scaffval  17530  rlmval  17837  rlmsca2  17847  2idlval  17881  rrgval  17935  asclfval  17983  psrplusg  18034  psrmulr  18037  psrvscafval  18043  mplval  18084  mplcoe3  18128  mplcoe3OLD  18129  evlval  18193  psr1val  18225  vr1val  18231  ply1val  18233  ply1basfvi  18282  ply1plusgfvi  18283  psr1sca2  18292  ply1sca2  18295  ply1ascl  18299  cply1mul  18335  gsummoncoe1  18346  evl1fval  18364  evl1fval1  18367  zrhval  18545  zlmlem  18554  zlmvsca  18559  chrval  18562  evpmss  18622  psgndiflemB  18636  ipffval  18683  thlbas  18727  thlle  18728  thloc  18730  pjfval  18737  dsmmval2  18767  mamufacex  18891  mavmulsolcl  19053  marrepfval  19062  marepvfval  19067  submafval  19081  mdetfval  19088  mdetfval1  19092  mdetunilem7  19120  mdetunilem8  19121  madufval  19139  minmar1fval  19148  mp2pm2mplem4  19310  tgdif0  19494  indislem  19501  resstopn  19687  iocpnfordt  19716  icomnfordt  19717  hmeofval  20259  ussval  20762  nmfval  21109  nghmfval  21229  pcofval  21510  tchval  21661  ioombl  21975  ibladdlem  22226  itgaddlem1  22229  iblabs  22235  dvbsss  22306  perfdvf  22307  mdegfval  22460  deg1fval  22480  deg1fvi  22485  uc1pval  22540  mon1pval  22542  ttglem  24179  axcontlem12  24278  usgraedgprv  24376  usgra1v  24390  nbusgra  24428  nbgra0nb  24429  nbgranself2  24436  cusgra1v  24461  uvtxisvtx  24490  uvtx0  24491  uvtx01vtx  24492  1conngra  24675  wwlknfi  24738  wlk0  24761  clwwlkprop  24770  clwwlkgt0  24771  clwwlknprop  24772  clwlkisclwwlklem2a4  24784  2wlkonot3v  24875  2spthonot3v  24876  vdgrf  24898  nbhashuvtx1  24915  frgra2v  24999  1to2vfriswmgra  25006  2pthfrgra  25011  frgrancvvdeqlem2  25031  2spotdisj  25061  2spotiundisj  25062  2spotmdisj  25068  frgrareggt1  25116  frgrareg  25117  frgraregord013  25118  frgraogt3nreg  25120  friendship  25122  avril1  25171  ismgmOLD  25322  vafval  25496  bafval  25497  smfval  25498  vsfval  25528  bcsiALT  26096  resvsca  27820  resvlem  27821  cntnevol  28199  signsw0glem  28510  mvtval  28860  mexval  28862  mexval2  28863  mdvval  28864  mrsubfval  28868  mrsubrn  28873  msubfval  28884  elmsubrn  28888  msubrn  28889  mvhfval  28893  mpstval  28895  msrfval  28897  mstaval  28904  mppsval  28932  mthmval  28935  dfrdg3  29229  trpredlem1  29310  bdayelon  29440  fvsingle  29570  unisnif  29575  funpartfv  29595  fullfunfv  29597  linedegen  29793  wl-nfs1t  29991  wl-sbcom3  30035  itg2addnclem  30066  ibladdnclem  30071  itgaddnclem1  30073  iblabsnc  30079  iblmulc2nc  30080  ftc1anclem8  30097  tsbi1  30540  tsbi2  30541  ac6s6  30580  mzpmfp  30679  mzpmfpOLD  30680  itgocn  31113  mendbas  31133  mendplusgfval  31134  mendmulrfval  31136  mendsca  31138  mendvscafval  31139  arearect  31183  areaquad  31184  addcomgi  31365  sqwvfoura  32011  sqwvfourb  32012  fourierswlem  32013  fouriersw  32014  tz6.12-afv  32258  ndmaovcl  32288  otiunsndisjX  32301  nzerooringczr  32880  pgrpgt2nabl  32959  suppmptcfin  32972  linc1  33026  lindslinindsimp2lem5  33063  ax6e2ndeq  33332  2sb5ndVD  33710  2sb5ndALT  33732  bnj1189  34065  bj-elimhyp  34160  bj-ax12v  34348  bj-hbs1  34352  bj-dtru  34383  bj-nfcsym  34460  bj-inftyexpidisj  34613  xptrrel  37775
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
  Copyright terms: Public domain W3C validator