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  1889  dvelimh  1904  exdistrf  1911  equveli  1928  dfsb2  1995  sbn  2002  sbi1  2003  sbco2  2026  sbco3  2028  sb9i  2034  ax11v  2036  hbs1  2044  nfsb  2048  sbal1  2065  sbal  2066  dvelimALT  2072  ax11  2094  equid1  2097  equid1ALT  2115  dvelimf-o  2119  ax11inda2ALT  2137  ax11inda2  2138  eujustALT  2146  moexex  2212  pm2.61ne  2521  pm2.61ine  2522  rgen2a  2609  ralcom2  2704  eueq2  2939  moeq3  2942  mo2icl  2944  sbc2or  2999  unineq  3419  ralidm  3557  ifsb  3574  ifid  3597  ifnot  3603  ifan  3604  ifor  3605  elimhyp  3613  elimhyp2v  3614  elimhyp3v  3615  elimhyp4v  3616  elimdhyp  3618  keephyp2v  3620  keephyp3v  3621  ssunsn2  3773  dfopif  3793  intabs  4172  class2set  4178  snexALT  4196  dtru  4201  dtruALT  4207  snex  4216  dtruALT2  4219  copsexg  4252  dfid3  4310  nsuceq0  4472  ordsssuc2  4481  unisn2  4522  ordsuc  4605  ordsucelsuc  4613  soirri  5069  soirriOLD  5074  dmsnopss  5145  dmsnsnsn  5151  opswap  5159  unixpid  5207  iotassuni  5235  iotaex  5236  dfiota4  5247  dffv3  5521  fvrn0  5550  ndmfv  5552  fveqres  5560  dffv2  5592  fvco4i  5597  fvmptss  5609  fvmptex  5610  fvmptss2  5619  f0cli  5671  fvunsn  5712  fconst5  5731  elimdelov  5927  ndmovcl  6005  ndmovord  6010  1stval  6124  2ndval  6125  1st2val  6145  2nd2val  6146  pwuninel  6300  riotav  6309  riotassuni  6343  smofvon2  6373  om0x  6518  brdomg  6872  snfi  6941  sdomirr  6998  domunsn  7011  2pwuninel  7016  fipwuni  7179  oicl  7244  oif  7245  card2on  7268  en2lp  7317  tctr  7425  r1tr  7448  rankdmr1  7473  r1pw  7517  r1pwOLD  7518  rankuni  7535  scottex  7555  cardidm  7592  alephcard  7697  alephnbtwn  7698  cdacomen  7807  cfub  7875  cardcf  7878  cflecard  7879  cfle  7880  cflim2  7889  cfidm  7901  isf32lem9  7987  itunisuc  8045  itunitc1  8046  itunitc  8047  ituniiun  8048  axcc2lem  8062  alephreg  8204  pwcfsdom  8205  cfpwsdom  8206  axunndlem1  8217  axpownd  8223  tskmcl  8463  addcompi  8518  addasspi  8519  mulcompi  8520  mulasspi  8521  distrpi  8522  addnidpi  8525  nlt1pi  8530  addcompq  8574  addcomnq  8575  mulcompq  8576  mulcomnq  8577  adderpq  8580  mulerpq  8581  addassnq  8582  mulassnq  8583  distrnq  8585  genpass  8633  addcompr  8645  mulcompr  8647  distrpr  8652  ltexprlem7  8666  addcomsr  8709  addasssr  8710  mulcomsr  8711  mulasssr  8712  distrsr  8713  uzssz  10247  uzwo  10281  uzwoOLD  10282  elixx3g  10669  iooid  10684  elfz2  10789  ltweuz  11024  fzofi  11036  hashsnlei  11376  swrd00  11451  gcdaddmlem  12707  pcmptcl  12939  strfvss  13166  strfvi  13186  setsnid  13188  ressbas  13198  ressbasss  13200  resslem  13201  ress0  13202  ressress  13205  strle1  13239  0rest  13334  firest  13337  topnval  13339  xpsaddlem  13477  xpsvsca  13481  homffval  13594  comfffval  13601  oppchomfval  13617  oppcbas  13621  fullfunc  13780  fthfunc  13781  natfval  13820  fucbas  13834  fuchom  13835  arwval  13875  coafval  13896  xpcbas  13952  xpchomfval  13953  xpccofval  13956  oduval  14234  oduleval  14235  odumeet  14244  odujoin  14246  ipopos  14263  plusffval  14379  grpidval  14384  gsum0  14457  frmdplusg  14476  frmd0  14482  grpinvfval  14520  grpinvfvi  14523  grpsubfval  14524  mulgfval  14568  mulgfvi  14571  symgbas  14772  symgplusg  14776  cntrval  14795  oppgval  14820  oppgplusfval  14821  odfval  14848  oppglsm  14953  efgval  15026  mgpval  15328  mgpplusg  15329  rngidval  15343  opprval  15406  opprmulfval  15407  dvdsrval  15427  invrfval  15455  dvrfval  15466  staffval  15612  scaffval  15645  rlmval  15945  rlmsca2  15953  2idlval  15985  rrgval  16028  asclfval  16074  psrplusg  16126  psrmulr  16129  psrvscafval  16135  mplval  16173  mplcoe3  16210  psr1val  16265  vr1val  16271  ply1val  16273  ply1basfvi  16319  ply1plusgfvi  16320  psr1sca2  16329  ply1sca2  16332  ply1ascl  16335  zrhval  16462  zlmlem  16471  zlmvsca  16476  chrval  16479  ipffval  16552  thlbas  16596  thlle  16597  thloc  16599  pjfval  16606  tgdif0  16730  indislem  16737  resstopn  16916  iocpnfordt  16945  icomnfordt  16946  hmeofval  17449  nmfval  18111  nghmfval  18231  pcofval  18508  tchval  18650  ioombl  18922  ibladdlem  19174  itgaddlem1  19177  iblabs  19183  limccnp2  19242  dvbsss  19252  perfdvf  19253  evlval  19408  evl1fval  19410  mdegfval  19448  deg1fval  19466  deg1fvi  19471  uc1pval  19525  mon1pval  19527  avril1  20836  ismgm  20987  vafval  21159  bafval  21160  smfval  21161  vsfval  21191  bcsiALT  21758  cntnevol  23175  dfrdg3  24153  trpredlem1  24230  bdayelon  24334  unisnif  24464  funpartfv  24483  fullfunfv  24485  axcontlem12  24603  linedegen  24766  elioo1t3  25502  oisbmi  25503  oisbmj  25504  oibbi1  25509  oibbi2  25510  intvconlem1  25703  hdrmp  25706  domval  25723  codval  25724  idval  25725  cmpval  25726  isconc2  26007  xsyysx  26145  bsstrs  26146  mzpmfp  26825  dsmmval2  27202  itgocn  27369  psgnfval  27423  mdetfval  27487  mendbas  27492  mendplusgfval  27493  mendmulrfval  27495  mendsca  27497  mendvscafval  27498  addcomgi  27661  ndmaovcl  28063  mpt2xopynvov0  28084  mpt2xopoveqd  28087  elprchashprn2  28088  usgraedgprv  28122  usgra1v  28126  nbusgra  28143  nbgra0nb  28144  nbgranself2  28151  cusgra1v  28157  uvtxisvtx  28162  uvtx0  28163  uvtx01vtx  28164  frgra2v  28177  1to2vfriswmgra  28184  a9e2ndeq  28325  2sb5ndVD  28686  2sb5ndALT  28709  bnj1189  29039  ax12-2  29103  a12lem1  29130  a12study11  29138  a12study11n  29139  ax9vax9  29158
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator