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

Theorem pm2.61i 158
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  |-  ( ph  ->  ps )
pm2.61i.2  |-  ( -. 
ph  ->  ps )
Assertion
Ref Expression
pm2.61i  |-  ps

Proof of Theorem pm2.61i
StepHypRef Expression
1 id 20 . 2  |-  ( ph  ->  ph )
2 pm2.61i.2 . . 3  |-  ( -. 
ph  ->  ps )
3 pm2.61i.1 . . 3  |-  ( ph  ->  ps )
42, 3ja 155 . 2  |-  ( (
ph  ->  ph )  ->  ps )
51, 4ax-mp 8 1  |-  ps
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  pm2.61ii  159  pm2.61nii  160  pm2.61iii  161  pm2.65i  167  pm5.21nii  343  pm5.18  346  biass  349  pm2.61ian  766  ecase3  908  4cases  916  elimh  923  pm4.42  927  3ecase  1288  a9e  1952  ax9OLD  2033  exdistrf  2062  exdistrfOLD  2063  dvelimhOLD  2068  equveliOLD  2082  dfsb2  2115  sbnOLD  2118  sbi1  2119  sbco2  2161  sbco3  2163  sb9i  2169  ax11v  2171  hbs1  2180  nfsb  2184  sbal1  2202  sbal  2203  dvelimALT  2209  ax11  2231  equid1  2234  equid1ALT  2252  dvelimf-o  2256  ax11inda2ALT  2274  ax11inda2  2275  eujustALT  2283  moexex  2349  pm2.61ne  2673  pm2.61ine  2674  rgen2a  2764  ralcom2  2864  eueq2  3100  moeq3  3103  mo2icl  3105  sbc2or  3161  unineq  3583  ralidm  3723  ifsb  3740  ifid  3763  ifnot  3769  ifan  3770  ifor  3771  elimhyp  3779  elimhyp2v  3780  elimhyp3v  3781  elimhyp4v  3782  elimdhyp  3784  keephyp2v  3786  keephyp3v  3787  rabrsn  3866  tppreqb  3931  ssunsn2  3950  dfopif  3973  intabs  4353  class2set  4359  snexALT  4377  dtru  4382  dtruALT  4388  snex  4397  dtruALT2  4400  copsexg  4434  dfid3  4491  nsuceq0  4653  ordsssuc2  4661  unisn2  4702  ordsuc  4785  ordsucelsuc  4793  soirri  5251  soirriOLD  5256  dmsnopss  5333  dmsnsnsn  5339  opswap  5347  unixpid  5395  iotassuni  5425  iotaex  5426  dfiota4  5437  dffv3  5715  fvrn0  5744  ndmfv  5746  fveqres  5755  dffv2  5787  fvco4i  5792  fvmptss  5804  fvmptex  5806  fvmptss2  5815  f0cli  5871  fvunsn  5916  fconst5  5940  0neqopab  6110  elimdelov  6144  ndmovcl  6223  ndmovord  6228  1stval  6342  2ndval  6343  1st2val  6363  2nd2val  6364  bropopvvv  6417  mpt2xopynvov0  6460  mpt2xopoveqd  6463  pwuninel  6536  riotav  6545  riotassuni  6579  smofvon2  6609  om0x  6754  brdomg  7109  snfi  7178  sdomirr  7235  domunsn  7248  2pwuninel  7253  fipwuni  7422  oicl  7487  oif  7488  card2on  7511  en2lp  7560  tctr  7668  r1tr  7691  rankdmr1  7716  r1pw  7760  r1pwOLD  7761  rankuni  7778  scottex  7798  cardidm  7835  alephcard  7940  alephnbtwn  7941  cdacomen  8050  cfub  8118  cardcf  8121  cflecard  8122  cfle  8123  cflim2  8132  cfidm  8144  isf32lem9  8230  itunisuc  8288  itunitc1  8289  itunitc  8290  ituniiun  8291  axcc2lem  8305  alephreg  8446  pwcfsdom  8447  cfpwsdom  8448  axunndlem1  8459  axpownd  8465  tskmcl  8705  addcompi  8760  addasspi  8761  mulcompi  8762  mulasspi  8763  distrpi  8764  addnidpi  8767  nlt1pi  8772  addcompq  8816  addcomnq  8817  mulcompq  8818  mulcomnq  8819  adderpq  8822  mulerpq  8823  addassnq  8824  mulassnq  8825  distrnq  8827  genpass  8875  addcompr  8887  mulcompr  8889  distrpr  8894  ltexprlem7  8908  addcomsr  8951  addasssr  8952  mulcomsr  8953  mulasssr  8954  distrsr  8955  uzssz  10494  uzwo  10528  uzwoOLD  10529  elixx3g  10918  iooid  10933  elfz2  11039  injresinjlem  11187  injresinj  11188  ltweuz  11289  fzofi  11301  hashrabrsn  11636  elprchashprn2  11655  hashsnlei  11668  hash1snb  11669  hashgt12el  11670  hashgt12el2  11671  swrd00  11753  gcdaddmlem  13016  pcmptcl  13248  strfvss  13475  strfvi  13495  setsnid  13497  ressbas  13507  ressbasss  13509  resslem  13510  ress0  13511  ressress  13514  strle1  13548  0rest  13645  firest  13648  topnval  13650  xpsaddlem  13788  xpsvsca  13792  homffval  13905  comfffval  13912  oppchomfval  13928  oppcbas  13932  fullfunc  14091  fthfunc  14092  natfval  14131  fucbas  14145  fuchom  14146  arwval  14186  coafval  14207  xpcbas  14263  xpchomfval  14264  xpccofval  14267  oduval  14545  oduleval  14546  odumeet  14555  odujoin  14557  ipopos  14574  plusffval  14690  grpidval  14695  gsum0  14768  frmdplusg  14787  frmd0  14793  grpinvfval  14831  grpinvfvi  14834  grpsubfval  14835  mulgfval  14879  mulgfvi  14882  symgbas  15083  symgplusg  15087  cntrval  15106  oppgval  15131  oppgplusfval  15132  odfval  15159  oppglsm  15264  efgval  15337  mgpval  15639  mgpplusg  15640  rngidval  15654  opprval  15717  opprmulfval  15718  dvdsrval  15738  invrfval  15766  dvrfval  15777  staffval  15923  scaffval  15956  rlmval  16252  rlmsca2  16260  2idlval  16292  rrgval  16335  asclfval  16381  psrplusg  16433  psrmulr  16436  psrvscafval  16442  mplval  16480  mplcoe3  16517  psr1val  16572  vr1val  16578  ply1val  16580  ply1basfvi  16623  ply1plusgfvi  16624  psr1sca2  16633  ply1sca2  16636  ply1ascl  16639  zrhval  16777  zlmlem  16786  zlmvsca  16791  chrval  16794  ipffval  16867  thlbas  16911  thlle  16912  thloc  16914  pjfval  16921  tgdif0  17045  indislem  17052  resstopn  17238  iocpnfordt  17267  icomnfordt  17268  hmeofval  17778  ussval  18277  nmfval  18624  nghmfval  18744  pcofval  19023  tchval  19165  ioombl  19447  ibladdlem  19699  itgaddlem1  19702  iblabs  19708  limccnp2  19767  dvbsss  19777  perfdvf  19778  evlval  19933  evl1fval  19935  mdegfval  19973  deg1fval  19991  deg1fvi  19996  uc1pval  20050  mon1pval  20052  usgraedgprv  21384  usgra1v  21397  nbusgra  21428  nbgra0nb  21429  nbgranself2  21436  cusgra1v  21458  uvtxisvtx  21487  uvtx0  21488  uvtx01vtx  21489  1conngra  21650  vdgrf  21657  avril1  21745  ismgm  21896  vafval  22070  bafval  22071  smfval  22072  vsfval  22102  bcsiALT  22669  cntnevol  24570  dfrdg3  25408  trpredlem1  25485  bdayelon  25589  fvsingle  25715  unisnif  25720  funpartfv  25740  fullfunfv  25742  axcontlem12  25862  linedegen  26025  itg2addnclem  26202  ibladdnclem  26207  itgaddnclem1  26209  iblabsnc  26215  iblmulc2nc  26216  mzpmfp  26741  dsmmval2  27117  itgocn  27284  psgnfval  27338  mdetfval  27402  mendbas  27407  mendplusgfval  27408  mendmulrfval  27410  mendsca  27412  mendvscafval  27413  addcomgi  27575  tz6.12-afv  27951  ndmaovcl  27981  otsndisj  28001  otiunsndisj  28002  otiunsndisjX  28003  euhash1  28071  swrdnd  28074  swrd0  28075  swrdccatin1  28091  swrdccatin12b  28102  swrdccatin12c  28103  swrdccat3b  28106  shwrd1  28161  shwrdssizelem1a  28165  shwrdssizelem2  28167  shwrdssize  28175  2wlkonot3v  28216  2spthonot3v  28217  frgra2v  28247  1to2vfriswmgra  28254  2pthfrgra  28259  frgrancvvdeqlem2  28278  2spotdisj  28308  2spotiundisj  28309  2spotmdisj  28315  a9e2ndeq  28501  2sb5ndVD  28876  2sb5ndALT  28899  bnj1189  29232  ax9NEW7  29322  dvelimhvAUX7  29346  exdistrfNEW7  29359  equveliNEW7  29380  sbnNEW7  29414  sbi1NEW7  29415  sbco2wAUX7  29436  sbco3wAUX7  29438  ax11vNEW7  29444  hbs1NEW7  29454  sbal1NEW7  29464  sbalNEW7  29465  dvelimALTNEW7  29485  dfsb2NEW7  29487  ax7w2AUX7  29499  ax7w6AUX7  29501  ax7w12AUX7  29514  dvelimhOLD7  29552  nfsbOLD7  29587  sbco2OLD7  29591  sbco3OLD7  29593  sb9iOLD7  29597
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator