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

Theorem pm2.61i 156
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 19 . 2  |-  ( ph  ->  ph )
2 pm2.61i.2 . . 3  |-  ( -. 
ph  ->  ps )
3 pm2.61i.1 . . 3  |-  ( ph  ->  ps )
42, 3ja 153 . 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  157  pm2.61nii  158  pm2.61iii  159  pm2.65i  165  pm5.21nii  342  pm5.18  345  biass  348  pm2.61ian  765  ecase3  907  4cases  915  elimh  922  pm4.42  926  3ecase  1286  ax9  1902  dvelimh  1917  exdistrf  1924  equveli  1941  dfsb2  2008  sbn  2015  sbi1  2016  sbco2  2039  sbco3  2041  sb9i  2047  ax11v  2049  hbs1  2057  nfsb  2061  sbal1  2078  sbal  2079  dvelimALT  2085  ax11  2107  equid1  2110  equid1ALT  2128  dvelimf-o  2132  ax11inda2ALT  2150  ax11inda2  2151  eujustALT  2159  moexex  2225  pm2.61ne  2534  pm2.61ine  2535  rgen2a  2622  ralcom2  2717  eueq2  2952  moeq3  2955  mo2icl  2957  sbc2or  3012  unineq  3432  ralidm  3570  ifsb  3587  ifid  3610  ifnot  3616  ifan  3617  ifor  3618  elimhyp  3626  elimhyp2v  3627  elimhyp3v  3628  elimhyp4v  3629  elimdhyp  3631  keephyp2v  3633  keephyp3v  3634  ssunsn2  3789  dfopif  3809  intabs  4188  class2set  4194  snexALT  4212  dtru  4217  dtruALT  4223  snex  4232  dtruALT2  4235  copsexg  4268  dfid3  4326  nsuceq0  4488  ordsssuc2  4497  unisn2  4538  ordsuc  4621  ordsucelsuc  4629  soirri  5085  soirriOLD  5090  dmsnopss  5161  dmsnsnsn  5167  opswap  5175  unixpid  5223  iotassuni  5251  iotaex  5252  dfiota4  5263  dffv3  5537  fvrn0  5566  ndmfv  5568  fveqres  5576  dffv2  5608  fvco4i  5613  fvmptss  5625  fvmptex  5626  fvmptss2  5635  f0cli  5687  fvunsn  5728  fconst5  5747  elimdelov  5943  ndmovcl  6021  ndmovord  6026  1stval  6140  2ndval  6141  1st2val  6161  2nd2val  6162  pwuninel  6316  riotav  6325  riotassuni  6359  smofvon2  6389  om0x  6534  brdomg  6888  snfi  6957  sdomirr  7014  domunsn  7027  2pwuninel  7032  fipwuni  7195  oicl  7260  oif  7261  card2on  7284  en2lp  7333  tctr  7441  r1tr  7464  rankdmr1  7489  r1pw  7533  r1pwOLD  7534  rankuni  7551  scottex  7571  cardidm  7608  alephcard  7713  alephnbtwn  7714  cdacomen  7823  cfub  7891  cardcf  7894  cflecard  7895  cfle  7896  cflim2  7905  cfidm  7917  isf32lem9  8003  itunisuc  8061  itunitc1  8062  itunitc  8063  ituniiun  8064  axcc2lem  8078  alephreg  8220  pwcfsdom  8221  cfpwsdom  8222  axunndlem1  8233  axpownd  8239  tskmcl  8479  addcompi  8534  addasspi  8535  mulcompi  8536  mulasspi  8537  distrpi  8538  addnidpi  8541  nlt1pi  8546  addcompq  8590  addcomnq  8591  mulcompq  8592  mulcomnq  8593  adderpq  8596  mulerpq  8597  addassnq  8598  mulassnq  8599  distrnq  8601  genpass  8649  addcompr  8661  mulcompr  8663  distrpr  8668  ltexprlem7  8682  addcomsr  8725  addasssr  8726  mulcomsr  8727  mulasssr  8728  distrsr  8729  uzssz  10263  uzwo  10297  uzwoOLD  10298  elixx3g  10685  iooid  10700  elfz2  10805  ltweuz  11040  fzofi  11052  hashsnlei  11392  swrd00  11467  gcdaddmlem  12723  pcmptcl  12955  strfvss  13182  strfvi  13202  setsnid  13204  ressbas  13214  ressbasss  13216  resslem  13217  ress0  13218  ressress  13221  strle1  13255  0rest  13350  firest  13353  topnval  13355  xpsaddlem  13493  xpsvsca  13497  homffval  13610  comfffval  13617  oppchomfval  13633  oppcbas  13637  fullfunc  13796  fthfunc  13797  natfval  13836  fucbas  13850  fuchom  13851  arwval  13891  coafval  13912  xpcbas  13968  xpchomfval  13969  xpccofval  13972  oduval  14250  oduleval  14251  odumeet  14260  odujoin  14262  ipopos  14279  plusffval  14395  grpidval  14400  gsum0  14473  frmdplusg  14492  frmd0  14498  grpinvfval  14536  grpinvfvi  14539  grpsubfval  14540  mulgfval  14584  mulgfvi  14587  symgbas  14788  symgplusg  14792  cntrval  14811  oppgval  14836  oppgplusfval  14837  odfval  14864  oppglsm  14969  efgval  15042  mgpval  15344  mgpplusg  15345  rngidval  15359  opprval  15422  opprmulfval  15423  dvdsrval  15443  invrfval  15471  dvrfval  15482  staffval  15628  scaffval  15661  rlmval  15961  rlmsca2  15969  2idlval  16001  rrgval  16044  asclfval  16090  psrplusg  16142  psrmulr  16145  psrvscafval  16151  mplval  16189  mplcoe3  16226  psr1val  16281  vr1val  16287  ply1val  16289  ply1basfvi  16335  ply1plusgfvi  16336  psr1sca2  16345  ply1sca2  16348  ply1ascl  16351  zrhval  16478  zlmlem  16487  zlmvsca  16492  chrval  16495  ipffval  16568  thlbas  16612  thlle  16613  thloc  16615  pjfval  16622  tgdif0  16746  indislem  16753  resstopn  16932  iocpnfordt  16961  icomnfordt  16962  hmeofval  17465  nmfval  18127  nghmfval  18247  pcofval  18524  tchval  18666  ioombl  18938  ibladdlem  19190  itgaddlem1  19193  iblabs  19199  limccnp2  19258  dvbsss  19268  perfdvf  19269  evlval  19424  evl1fval  19426  mdegfval  19464  deg1fval  19482  deg1fvi  19487  uc1pval  19541  mon1pval  19543  avril1  20852  ismgm  21003  vafval  21175  bafval  21176  smfval  21177  vsfval  21207  bcsiALT  21774  cntnevol  23191  dfrdg3  24224  trpredlem1  24301  bdayelon  24405  unisnif  24535  funpartfv  24555  fullfunfv  24557  axcontlem12  24675  linedegen  24838  itg2addnclem  25003  ibladdnclem  25007  itgaddnclem1  25009  iblabsnc  25015  iblmulc2nc  25016  elioo1t3  25605  oisbmi  25606  oisbmj  25607  oibbi1  25612  oibbi2  25613  intvconlem1  25806  hdrmp  25809  domval  25826  codval  25827  idval  25828  cmpval  25829  isconc2  26110  xsyysx  26248  bsstrs  26249  mzpmfp  26928  dsmmval2  27305  itgocn  27472  psgnfval  27526  mdetfval  27590  mendbas  27595  mendplusgfval  27596  mendmulrfval  27598  mendsca  27600  mendvscafval  27601  addcomgi  27764  tz6.12-afv  28141  ndmaovcl  28171  0neqopab  28192  mpt2xopynvov0  28200  mpt2xopoveqd  28203  injresinjlem  28214  injresinj  28215  elprchashprn2  28216  hashgt12el  28218  hashgt12el2  28219  usgraedgprv  28256  usgra1v  28260  nbusgra  28277  nbgra0nb  28278  nbgranself2  28285  cusgra1v  28296  uvtxisvtx  28303  uvtx0  28304  uvtx01vtx  28305  trlonprop  28341  frgra2v  28423  1to2vfriswmgra  28430  a9e2ndeq  28624  2sb5ndVD  29002  2sb5ndALT  29025  bnj1189  29355  ax9NEW7  29445  dvelimhvAUX7  29469  exdistrfNEW7  29482  equveliNEW7  29503  sbnNEW7  29537  sbi1NEW7  29538  sbco2wAUX7  29559  sbco3wAUX7  29561  ax11vNEW7  29567  hbs1NEW7  29577  sbal1NEW7  29587  sbalNEW7  29588  dfsb2NEW7  29609  ax7w2AUX7  29620  ax7w6AUX7  29622  dvelimhOLD7  29667  nfsbOLD7  29702  sbco2OLD7  29706  sbco3OLD7  29708  sb9iOLD7  29712  ax12-2  29725  a12lem1  29752  a12study11  29760  a12study11n  29761  ax9vax9  29780
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator