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  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  4662  unisn2  4703  ordsuc  4786  ordsucelsuc  4794  soirri  5252  soirriOLD  5257  dmsnopss  5334  dmsnsnsn  5340  opswap  5348  unixpid  5396  iotassuni  5426  iotaex  5427  dfiota4  5438  dffv3  5716  fvrn0  5745  ndmfv  5747  fveqres  5756  dffv2  5788  fvco4i  5793  fvmptss  5805  fvmptex  5807  fvmptss2  5816  f0cli  5872  fvunsn  5917  fconst5  5941  0neqopab  6111  elimdelov  6145  ndmovcl  6224  ndmovord  6229  1stval  6343  2ndval  6344  1st2val  6364  2nd2val  6365  bropopvvv  6418  mpt2xopynvov0  6461  mpt2xopoveqd  6464  pwuninel  6537  riotav  6546  riotassuni  6580  smofvon2  6610  om0x  6755  brdomg  7110  snfi  7179  sdomirr  7236  domunsn  7249  2pwuninel  7254  fipwuni  7423  oicl  7490  oif  7491  card2on  7514  en2lp  7563  tctr  7671  r1tr  7694  rankdmr1  7719  r1pw  7763  r1pwOLD  7764  rankuni  7781  scottex  7801  cardidm  7838  alephcard  7943  alephnbtwn  7944  cdacomen  8053  cfub  8121  cardcf  8124  cflecard  8125  cfle  8126  cflim2  8135  cfidm  8147  isf32lem9  8233  itunisuc  8291  itunitc1  8292  itunitc  8293  ituniiun  8294  axcc2lem  8308  alephreg  8449  pwcfsdom  8450  cfpwsdom  8451  axunndlem1  8462  axpownd  8468  tskmcl  8708  addcompi  8763  addasspi  8764  mulcompi  8765  mulasspi  8766  distrpi  8767  addnidpi  8770  nlt1pi  8775  addcompq  8819  addcomnq  8820  mulcompq  8821  mulcomnq  8822  adderpq  8825  mulerpq  8826  addassnq  8827  mulassnq  8828  distrnq  8830  genpass  8878  addcompr  8890  mulcompr  8892  distrpr  8897  ltexprlem7  8911  addcomsr  8954  addasssr  8955  mulcomsr  8956  mulasssr  8957  distrsr  8958  uzssz  10497  uzwo  10531  uzwoOLD  10532  elixx3g  10921  iooid  10936  elfz2  11042  injresinjlem  11191  injresinj  11192  ltweuz  11293  fzofi  11305  hashrabrsn  11640  elprchashprn2  11659  hashsnlei  11672  hash1snb  11673  hashgt12el  11674  hashgt12el2  11675  swrd00  11757  gcdaddmlem  13020  pcmptcl  13252  strfvss  13479  strfvi  13499  setsnid  13501  ressbas  13511  ressbasss  13513  resslem  13514  ress0  13515  ressress  13518  strle1  13552  0rest  13649  firest  13652  topnval  13654  xpsaddlem  13792  xpsvsca  13796  homffval  13909  comfffval  13916  oppchomfval  13932  oppcbas  13936  fullfunc  14095  fthfunc  14096  natfval  14135  fucbas  14149  fuchom  14150  arwval  14190  coafval  14211  xpcbas  14267  xpchomfval  14268  xpccofval  14271  oduval  14549  oduleval  14550  odumeet  14559  odujoin  14561  ipopos  14578  plusffval  14694  grpidval  14699  gsum0  14772  frmdplusg  14791  frmd0  14797  grpinvfval  14835  grpinvfvi  14838  grpsubfval  14839  mulgfval  14883  mulgfvi  14886  symgbas  15087  symgplusg  15091  cntrval  15110  oppgval  15135  oppgplusfval  15136  odfval  15163  oppglsm  15268  efgval  15341  mgpval  15643  mgpplusg  15644  rngidval  15658  opprval  15721  opprmulfval  15722  dvdsrval  15742  invrfval  15770  dvrfval  15781  staffval  15927  scaffval  15960  rlmval  16256  rlmsca2  16264  2idlval  16296  rrgval  16339  asclfval  16385  psrplusg  16437  psrmulr  16440  psrvscafval  16446  mplval  16484  mplcoe3  16521  psr1val  16576  vr1val  16582  ply1val  16584  ply1basfvi  16627  ply1plusgfvi  16628  psr1sca2  16637  ply1sca2  16640  ply1ascl  16643  zrhval  16781  zlmlem  16790  zlmvsca  16795  chrval  16798  ipffval  16871  thlbas  16915  thlle  16916  thloc  16918  pjfval  16925  tgdif0  17049  indislem  17056  resstopn  17242  iocpnfordt  17271  icomnfordt  17272  hmeofval  17782  ussval  18281  nmfval  18628  nghmfval  18748  pcofval  19027  tchval  19169  ioombl  19451  ibladdlem  19703  itgaddlem1  19706  iblabs  19712  limccnp2  19771  dvbsss  19781  perfdvf  19782  evlval  19937  evl1fval  19939  mdegfval  19977  deg1fval  19995  deg1fvi  20000  uc1pval  20054  mon1pval  20056  usgraedgprv  21388  usgra1v  21401  nbusgra  21432  nbgra0nb  21433  nbgranself2  21440  cusgra1v  21462  uvtxisvtx  21491  uvtx0  21492  uvtx01vtx  21493  1conngra  21654  vdgrf  21661  avril1  21749  ismgm  21900  vafval  22074  bafval  22075  smfval  22076  vsfval  22106  bcsiALT  22673  cntnevol  24574  dfrdg3  25416  trpredlem1  25497  bdayelon  25627  fvsingle  25757  unisnif  25762  funpartfv  25782  fullfunfv  25784  axcontlem12  25906  linedegen  26069  itg2addnclem  26246  ibladdnclem  26251  itgaddnclem1  26253  iblabsnc  26259  iblmulc2nc  26260  ftc1anclem5  26274  ftc1anclem8  26277  mzpmfp  26795  dsmmval2  27170  itgocn  27337  psgnfval  27391  mdetfval  27455  mendbas  27460  mendplusgfval  27461  mendmulrfval  27463  mendsca  27465  mendvscafval  27466  addcomgi  27628  tz6.12-afv  28004  ndmaovcl  28034  otsndisj  28055  otiunsndisj  28056  otiunsndisjX  28057  modifeq2int  28139  euhash1  28145  ccatsymb  28152  swrdnd  28154  swrd0  28155  swrdccatin1  28171  cshwcl  28206  2cshwmod  28223  cshw1  28238  cshwssizelem1a  28242  cshwssizelem2  28244  cshwssize  28253  2wlkonot3v  28295  2spthonot3v  28296  frgra2v  28326  1to2vfriswmgra  28333  2pthfrgra  28338  frgrancvvdeqlem2  28357  2spotdisj  28387  2spotiundisj  28388  2spotmdisj  28394  a9e2ndeq  28583  2sb5ndVD  28959  2sb5ndALT  28981  bnj1189  29315  ax9NEW7  29405  dvelimhvAUX7  29429  exdistrfNEW7  29442  equveliNEW7  29465  sbnNEW7  29499  sbi1NEW7  29500  sbco2wAUX7  29522  sbco3wAUX7  29524  ax11vNEW7  29532  hbs1NEW7  29542  sbal1NEW7  29552  sbalNEW7  29553  dvelimALTNEW7  29573  dfsb2NEW7  29575  ax7w2AUX7  29587  ax7w6AUX7  29589  nfsbwAUX7  29602  ax7w14AUX7  29607  dvelimhOLD7  29650  nfsbOLD7  29685  sbco2OLD7  29689  sbco3OLD7  29691  sb9iOLD7  29695
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator