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  1941  ax9-OLD  1981  dvelimh  1990  exdistrf  1997  equveli  2014  dfsb2  2081  sbn  2088  sbi1  2089  sbco2  2112  sbco3  2114  sb9i  2120  ax11v  2122  hbs1  2131  nfsb  2135  sbal1  2153  sbal  2154  dvelimALT  2160  ax11  2182  equid1  2185  equid1ALT  2203  dvelimf-o  2207  ax11inda2ALT  2225  ax11inda2  2226  eujustALT  2234  moexex  2300  pm2.61ne  2618  pm2.61ine  2619  rgen2a  2708  ralcom2  2808  eueq2  3044  moeq3  3047  mo2icl  3049  sbc2or  3105  unineq  3527  ralidm  3667  ifsb  3684  ifid  3707  ifnot  3713  ifan  3714  ifor  3715  elimhyp  3723  elimhyp2v  3724  elimhyp3v  3725  elimhyp4v  3726  elimdhyp  3728  keephyp2v  3730  keephyp3v  3731  rabrsn  3810  tppreqb  3875  ssunsn2  3894  dfopif  3916  intabs  4295  class2set  4301  snexALT  4319  dtru  4324  dtruALT  4330  snex  4339  dtruALT2  4342  copsexg  4376  dfid3  4433  nsuceq0  4595  ordsssuc2  4603  unisn2  4644  ordsuc  4727  ordsucelsuc  4735  soirri  5193  soirriOLD  5198  dmsnopss  5275  dmsnsnsn  5281  opswap  5289  unixpid  5337  iotassuni  5367  iotaex  5368  dfiota4  5379  dffv3  5657  fvrn0  5686  ndmfv  5688  fveqres  5696  dffv2  5728  fvco4i  5733  fvmptss  5745  fvmptex  5747  fvmptss2  5756  f0cli  5812  fvunsn  5857  fconst5  5881  0neqopab  6051  elimdelov  6085  ndmovcl  6164  ndmovord  6169  1stval  6283  2ndval  6284  1st2val  6304  2nd2val  6305  bropopvvv  6358  mpt2xopynvov0  6398  mpt2xopoveqd  6401  pwuninel  6474  riotav  6483  riotassuni  6517  smofvon2  6547  om0x  6692  brdomg  7047  snfi  7116  sdomirr  7173  domunsn  7186  2pwuninel  7191  fipwuni  7359  oicl  7424  oif  7425  card2on  7448  en2lp  7497  tctr  7605  r1tr  7628  rankdmr1  7653  r1pw  7697  r1pwOLD  7698  rankuni  7715  scottex  7735  cardidm  7772  alephcard  7877  alephnbtwn  7878  cdacomen  7987  cfub  8055  cardcf  8058  cflecard  8059  cfle  8060  cflim2  8069  cfidm  8081  isf32lem9  8167  itunisuc  8225  itunitc1  8226  itunitc  8227  ituniiun  8228  axcc2lem  8242  alephreg  8383  pwcfsdom  8384  cfpwsdom  8385  axunndlem1  8396  axpownd  8402  tskmcl  8642  addcompi  8697  addasspi  8698  mulcompi  8699  mulasspi  8700  distrpi  8701  addnidpi  8704  nlt1pi  8709  addcompq  8753  addcomnq  8754  mulcompq  8755  mulcomnq  8756  adderpq  8759  mulerpq  8760  addassnq  8761  mulassnq  8762  distrnq  8764  genpass  8812  addcompr  8824  mulcompr  8826  distrpr  8831  ltexprlem7  8845  addcomsr  8888  addasssr  8889  mulcomsr  8890  mulasssr  8891  distrsr  8892  uzssz  10430  uzwo  10464  uzwoOLD  10465  elixx3g  10854  iooid  10869  elfz2  10975  injresinjlem  11119  injresinj  11120  ltweuz  11221  fzofi  11233  hashrabrsn  11568  elprchashprn2  11587  hashsnlei  11600  hash1snb  11601  hashgt12el  11602  hashgt12el2  11603  swrd00  11685  gcdaddmlem  12948  pcmptcl  13180  strfvss  13407  strfvi  13427  setsnid  13429  ressbas  13439  ressbasss  13441  resslem  13442  ress0  13443  ressress  13446  strle1  13480  0rest  13577  firest  13580  topnval  13582  xpsaddlem  13720  xpsvsca  13724  homffval  13837  comfffval  13844  oppchomfval  13860  oppcbas  13864  fullfunc  14023  fthfunc  14024  natfval  14063  fucbas  14077  fuchom  14078  arwval  14118  coafval  14139  xpcbas  14195  xpchomfval  14196  xpccofval  14199  oduval  14477  oduleval  14478  odumeet  14487  odujoin  14489  ipopos  14506  plusffval  14622  grpidval  14627  gsum0  14700  frmdplusg  14719  frmd0  14725  grpinvfval  14763  grpinvfvi  14766  grpsubfval  14767  mulgfval  14811  mulgfvi  14814  symgbas  15015  symgplusg  15019  cntrval  15038  oppgval  15063  oppgplusfval  15064  odfval  15091  oppglsm  15196  efgval  15269  mgpval  15571  mgpplusg  15572  rngidval  15586  opprval  15649  opprmulfval  15650  dvdsrval  15670  invrfval  15698  dvrfval  15709  staffval  15855  scaffval  15888  rlmval  16184  rlmsca2  16192  2idlval  16224  rrgval  16267  asclfval  16313  psrplusg  16365  psrmulr  16368  psrvscafval  16374  mplval  16412  mplcoe3  16449  psr1val  16504  vr1val  16510  ply1val  16512  ply1basfvi  16555  ply1plusgfvi  16556  psr1sca2  16565  ply1sca2  16568  ply1ascl  16571  zrhval  16705  zlmlem  16714  zlmvsca  16719  chrval  16722  ipffval  16795  thlbas  16839  thlle  16840  thloc  16842  pjfval  16849  tgdif0  16973  indislem  16980  resstopn  17165  iocpnfordt  17194  icomnfordt  17195  hmeofval  17704  ussval  18203  nmfval  18500  nghmfval  18620  pcofval  18899  tchval  19041  ioombl  19319  ibladdlem  19571  itgaddlem1  19574  iblabs  19580  limccnp2  19639  dvbsss  19649  perfdvf  19650  evlval  19805  evl1fval  19807  mdegfval  19845  deg1fval  19863  deg1fvi  19868  uc1pval  19922  mon1pval  19924  usgraedgprv  21256  usgra1v  21268  nbusgra  21299  nbgra0nb  21300  nbgranself2  21307  cusgra1v  21329  uvtxisvtx  21358  uvtx0  21359  uvtx01vtx  21360  1conngra  21503  vdgrf  21510  avril1  21598  ismgm  21749  vafval  21923  bafval  21924  smfval  21925  vsfval  21955  bcsiALT  22522  cntnevol  24369  dfrdg3  25170  trpredlem1  25247  bdayelon  25351  unisnif  25481  funpartfv  25501  fullfunfv  25503  axcontlem12  25621  linedegen  25784  itg2addnclem  25950  ibladdnclem  25954  itgaddnclem1  25956  iblabsnc  25962  iblmulc2nc  25963  mzpmfp  26488  dsmmval2  26864  itgocn  27031  psgnfval  27085  mdetfval  27149  mendbas  27154  mendplusgfval  27155  mendmulrfval  27157  mendsca  27159  mendvscafval  27160  addcomgi  27322  tz6.12-afv  27699  ndmaovcl  27729  frgra2v  27745  1to2vfriswmgra  27752  2pthfrgra  27757  frgrancvvdeqlem2  27776  a9e2ndeq  27982  2sb5ndVD  28356  2sb5ndALT  28379  bnj1189  28709  ax9NEW7  28799  dvelimhvAUX7  28823  exdistrfNEW7  28836  equveliNEW7  28857  sbnNEW7  28891  sbi1NEW7  28892  sbco2wAUX7  28913  sbco3wAUX7  28915  ax11vNEW7  28921  hbs1NEW7  28931  sbal1NEW7  28941  sbalNEW7  28942  dvelimALTNEW7  28962  dfsb2NEW7  28964  ax7w2AUX7  28975  ax7w6AUX7  28977  dvelimhOLD7  29022  nfsbOLD7  29057  sbco2OLD7  29061  sbco3OLD7  29063  sb9iOLD7  29067  ax12-2  29079  a12lem1  29106  a12study11  29114  a12study11n  29115  ax9vax9  29134
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator