MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm2.61i Structured version   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  2066  exdistrfOLD  2067  dvelimhOLD  2072  equveliOLD  2086  dfsb2  2108  sbnOLD  2131  sbi1  2132  sbco2  2161  sbco3  2163  sb9i  2170  ax11v  2172  hbs1  2181  nfsb  2185  sbal1  2203  sbal  2204  dvelimALT  2210  ax11  2232  equid1  2235  equid1ALT  2253  dvelimf-o  2257  ax11inda2ALT  2275  ax11inda2  2276  eujustALT  2284  moexex  2350  pm2.61ne  2679  pm2.61ine  2680  rgen2a  2772  ralcom2  2872  eueq2  3108  moeq3  3111  mo2icl  3113  sbc2or  3169  unineq  3591  ralidm  3731  ifsb  3748  ifid  3771  ifnot  3777  ifan  3778  ifor  3779  elimhyp  3787  elimhyp2v  3788  elimhyp3v  3789  elimhyp4v  3790  elimdhyp  3792  keephyp2v  3794  keephyp3v  3795  rabrsn  3874  tppreqb  3939  ssunsn2  3958  dfopif  3981  intabs  4361  class2set  4367  snexALT  4385  dtru  4390  dtruALT  4396  snex  4405  dtruALT2  4408  copsexg  4442  dfid3  4499  nsuceq0  4661  ordsssuc2  4670  unisn2  4711  ordsuc  4794  ordsucelsuc  4802  soirri  5260  soirriOLD  5265  dmsnopss  5342  dmsnsnsn  5348  opswap  5356  unixpid  5404  iotassuni  5434  iotaex  5435  dfiota4  5446  dffv3  5724  fvrn0  5753  ndmfv  5755  fveqres  5764  dffv2  5796  fvco4i  5801  fvmptss  5813  fvmptex  5815  fvmptss2  5824  f0cli  5880  fvunsn  5925  fconst5  5949  0neqopab  6119  elimdelov  6153  ndmovcl  6232  ndmovord  6237  1stval  6351  2ndval  6352  1st2val  6372  2nd2val  6373  bropopvvv  6426  mpt2xopynvov0  6469  mpt2xopoveqd  6472  pwuninel  6545  riotav  6554  riotassuni  6588  smofvon2  6618  om0x  6763  brdomg  7118  snfi  7187  sdomirr  7244  domunsn  7257  2pwuninel  7262  fipwuni  7431  oicl  7498  oif  7499  card2on  7522  en2lp  7571  tctr  7679  r1tr  7702  rankdmr1  7727  r1pw  7771  r1pwOLD  7772  rankuni  7789  scottex  7809  cardidm  7846  alephcard  7951  alephnbtwn  7952  cdacomen  8061  cfub  8129  cardcf  8132  cflecard  8133  cfle  8134  cflim2  8143  cfidm  8155  isf32lem9  8241  itunisuc  8299  itunitc1  8300  itunitc  8301  ituniiun  8302  axcc2lem  8316  alephreg  8457  pwcfsdom  8458  cfpwsdom  8459  axunndlem1  8470  axpownd  8476  tskmcl  8716  addcompi  8771  addasspi  8772  mulcompi  8773  mulasspi  8774  distrpi  8775  addnidpi  8778  nlt1pi  8783  addcompq  8827  addcomnq  8828  mulcompq  8829  mulcomnq  8830  adderpq  8833  mulerpq  8834  addassnq  8835  mulassnq  8836  distrnq  8838  genpass  8886  addcompr  8898  mulcompr  8900  distrpr  8905  ltexprlem7  8919  addcomsr  8962  addasssr  8963  mulcomsr  8964  mulasssr  8965  distrsr  8966  uzssz  10505  uzwo  10539  uzwoOLD  10540  elixx3g  10929  iooid  10944  elfz2  11050  injresinjlem  11199  injresinj  11200  ltweuz  11301  fzofi  11313  hashrabrsn  11648  elprchashprn2  11667  hashsnlei  11680  hash1snb  11681  hashgt12el  11682  hashgt12el2  11683  swrd00  11765  gcdaddmlem  13028  pcmptcl  13260  strfvss  13487  strfvi  13507  setsnid  13509  ressbas  13519  ressbasss  13521  resslem  13522  ress0  13523  ressress  13526  strle1  13560  0rest  13657  firest  13660  topnval  13662  xpsaddlem  13800  xpsvsca  13804  homffval  13917  comfffval  13924  oppchomfval  13940  oppcbas  13944  fullfunc  14103  fthfunc  14104  natfval  14143  fucbas  14157  fuchom  14158  arwval  14198  coafval  14219  xpcbas  14275  xpchomfval  14276  xpccofval  14279  oduval  14557  oduleval  14558  odumeet  14567  odujoin  14569  ipopos  14586  plusffval  14702  grpidval  14707  gsum0  14780  frmdplusg  14799  frmd0  14805  grpinvfval  14843  grpinvfvi  14846  grpsubfval  14847  mulgfval  14891  mulgfvi  14894  symgbas  15095  symgplusg  15099  cntrval  15118  oppgval  15143  oppgplusfval  15144  odfval  15171  oppglsm  15276  efgval  15349  mgpval  15651  mgpplusg  15652  rngidval  15666  opprval  15729  opprmulfval  15730  dvdsrval  15750  invrfval  15778  dvrfval  15789  staffval  15935  scaffval  15968  rlmval  16264  rlmsca2  16272  2idlval  16304  rrgval  16347  asclfval  16393  psrplusg  16445  psrmulr  16448  psrvscafval  16454  mplval  16492  mplcoe3  16529  psr1val  16584  vr1val  16590  ply1val  16592  ply1basfvi  16635  ply1plusgfvi  16636  psr1sca2  16645  ply1sca2  16648  ply1ascl  16651  zrhval  16789  zlmlem  16798  zlmvsca  16803  chrval  16806  ipffval  16879  thlbas  16923  thlle  16924  thloc  16926  pjfval  16933  tgdif0  17057  indislem  17064  resstopn  17250  iocpnfordt  17279  icomnfordt  17280  hmeofval  17790  ussval  18289  nmfval  18636  nghmfval  18756  pcofval  19035  tchval  19177  ioombl  19459  ibladdlem  19711  itgaddlem1  19714  iblabs  19720  limccnp2  19779  dvbsss  19789  perfdvf  19790  evlval  19945  evl1fval  19947  mdegfval  19985  deg1fval  20003  deg1fvi  20008  uc1pval  20062  mon1pval  20064  usgraedgprv  21396  usgra1v  21409  nbusgra  21440  nbgra0nb  21441  nbgranself2  21448  cusgra1v  21470  uvtxisvtx  21499  uvtx0  21500  uvtx01vtx  21501  1conngra  21662  vdgrf  21669  avril1  21757  ismgm  21908  vafval  22082  bafval  22083  smfval  22084  vsfval  22114  bcsiALT  22681  cntnevol  24582  dfrdg3  25424  trpredlem1  25505  bdayelon  25635  fvsingle  25765  unisnif  25770  funpartfv  25790  fullfunfv  25792  axcontlem12  25914  linedegen  26077  itg2addnclem  26256  ibladdnclem  26261  itgaddnclem1  26263  iblabsnc  26269  iblmulc2nc  26270  ftc1anclem5  26284  ftc1anclem8  26287  mzpmfp  26804  dsmmval2  27179  itgocn  27346  psgnfval  27400  mdetfval  27464  mendbas  27469  mendplusgfval  27470  mendmulrfval  27472  mendsca  27474  mendvscafval  27475  addcomgi  27637  tz6.12-afv  28013  ndmaovcl  28043  otsndisj  28065  otiunsndisj  28066  otiunsndisjX  28067  modifeq2int  28161  euhash1  28167  ccatsymb  28179  swrdnd  28182  swrd0  28183  swrdccatin1  28205  cshwcl  28240  2cshwmod  28257  cshw1  28275  cshwssizelem1a  28279  cshwssizelem2  28281  cshwssize  28290  2wlkonot3v  28342  2spthonot3v  28343  frgra2v  28389  1to2vfriswmgra  28396  2pthfrgra  28401  frgrancvvdeqlem2  28420  2spotdisj  28450  2spotiundisj  28451  2spotmdisj  28457  a9e2ndeq  28646  2sb5ndVD  29022  2sb5ndALT  29044  bnj1189  29378  ax9NEW7  29468  dvelimhvAUX7  29492  exdistrfNEW7  29505  equveliNEW7  29528  sbnNEW7  29562  sbi1NEW7  29563  sbco2wAUX7  29585  sbco3wAUX7  29587  ax11vNEW7  29595  hbs1NEW7  29605  sbal1NEW7  29615  sbalNEW7  29616  dvelimALTNEW7  29636  dfsb2NEW7  29638  ax7w2AUX7  29650  ax7w6AUX7  29652  nfsbwAUX7  29665  ax7w14AUX7  29670  dvelimhOLD7  29713  nfsbOLD7  29748  sbco2OLD7  29752  sbco3OLD7  29754  sb9iOLD7  29758
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator