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  1891  dvelimfALT  1907  exdistrf  1914  equveli  1931  dfsb2  1994  sbn  2001  sbi1  2002  sbco2  2025  sbco3  2027  sb9i  2033  ax11v  2036  hbs1  2044  nfsb  2051  sbal1  2068  sbal  2069  dvelimALT  2075  ax11  2096  equid1  2099  equid1ALT  2117  dvelimf-o  2121  ax11inda2ALT  2138  ax11inda2  2139  eujustALT  2147  moexex  2213  pm2.61ne  2522  pm2.61ine  2523  rgen2a  2610  ralcom2  2705  eueq2  2940  moeq3  2943  mo2icl  2945  sbc2or  3000  unineq  3420  ralidm  3558  ifsb  3575  ifid  3598  ifnot  3604  ifan  3605  ifor  3606  elimhyp  3614  elimhyp2v  3615  elimhyp3v  3616  elimhyp4v  3617  elimdhyp  3619  keephyp2v  3621  keephyp3v  3622  ssunsn2  3774  dfopif  3794  intabs  4175  class2set  4177  snexALT  4195  dtru  4200  dtruALT  4206  snex  4215  dtruALT2  4218  copsexg  4251  dfid3  4309  nsuceq0  4471  ordsssuc2  4480  unisn2  4521  ordsuc  4604  ordsucelsuc  4612  soirri  5068  soirriOLD  5073  dmsnopss  5143  dmsnsnsn  5149  opswap  5157  unixpid  5205  fv2  5482  fvrn0  5512  fveqres  5522  dffv2  5554  fvco4i  5559  fvmptss  5571  fvmptex  5572  fvmptss2  5581  f0cli  5633  fvunsn  5674  fconst5  5693  elimdelov  5889  ndmovcl  5967  ndmovord  5972  1stval  6086  2ndval  6087  1st2val  6107  2nd2val  6108  iotassuni  6269  iotaex  6270  pwuninel  6296  riotav  6305  riotassuni  6339  smofvon2  6369  om0x  6514  brdomg  6868  snfi  6937  sdomirr  6994  domunsn  7007  2pwuninel  7012  fipwuni  7175  oicl  7240  oif  7241  card2on  7264  en2lp  7313  tctr  7421  r1tr  7444  rankdmr1  7469  r1pw  7513  r1pwOLD  7514  rankuni  7531  scottex  7551  cardidm  7588  alephcard  7693  alephnbtwn  7694  cdacomen  7803  cfub  7871  cardcf  7874  cflecard  7875  cfle  7876  cflim2  7885  cfidm  7897  isf32lem9  7983  itunisuc  8041  itunitc1  8042  itunitc  8043  ituniiun  8044  axcc2lem  8058  alephreg  8200  pwcfsdom  8201  cfpwsdom  8202  axunndlem1  8213  axpownd  8219  tskmcl  8459  addcompi  8514  addasspi  8515  mulcompi  8516  mulasspi  8517  distrpi  8518  addnidpi  8521  nlt1pi  8526  addcompq  8570  addcomnq  8571  mulcompq  8572  mulcomnq  8573  adderpq  8576  mulerpq  8577  addassnq  8578  mulassnq  8579  distrnq  8581  genpass  8629  addcompr  8641  mulcompr  8643  distrpr  8648  ltexprlem7  8662  addcomsr  8705  addasssr  8706  mulcomsr  8707  mulasssr  8708  distrsr  8709  uzssz  10243  uzwo  10277  uzwoOLD  10278  elixx3g  10665  iooid  10680  elfz2  10785  ltweuz  11020  fzofi  11032  hashsnlei  11372  swrd00  11447  gcdaddmlem  12703  pcmptcl  12935  strfvss  13162  strfvi  13182  setsnid  13184  ressbas  13194  ressbasss  13196  resslem  13197  ress0  13198  ressress  13201  strle1  13235  0rest  13330  firest  13333  topnval  13335  xpsaddlem  13473  xpsvsca  13477  homffval  13590  comfffval  13597  oppchomfval  13613  oppcbas  13617  fullfunc  13776  fthfunc  13777  natfval  13816  fucbas  13830  fuchom  13831  arwval  13871  coafval  13892  xpcbas  13948  xpchomfval  13949  xpccofval  13952  oduval  14230  oduleval  14231  odumeet  14240  odujoin  14242  ipopos  14259  plusffval  14375  grpidval  14380  gsum0  14453  frmdplusg  14472  frmd0  14478  grpinvfval  14516  grpinvfvi  14519  grpsubfval  14520  mulgfval  14564  mulgfvi  14567  symgbas  14768  symgplusg  14772  cntrval  14791  oppgval  14816  oppgplusfval  14817  odfval  14844  oppglsm  14949  efgval  15022  mgpval  15324  mgpplusg  15325  rngidval  15339  opprval  15402  opprmulfval  15403  dvdsrval  15423  invrfval  15451  dvrfval  15462  staffval  15608  scaffval  15641  rlmval  15941  rlmsca2  15949  2idlval  15981  rrgval  16024  asclfval  16070  psrplusg  16122  psrmulr  16125  psrvscafval  16131  mplval  16169  mplcoe3  16206  psr1val  16261  vr1val  16267  ply1val  16269  ply1basfvi  16315  ply1plusgfvi  16316  psr1sca2  16325  ply1sca2  16328  ply1ascl  16331  zrhval  16458  zlmlem  16467  zlmvsca  16472  chrval  16475  ipffval  16548  thlbas  16592  thlle  16593  thloc  16595  pjfval  16602  tgdif0  16726  indislem  16733  resstopn  16912  iocpnfordt  16941  icomnfordt  16942  hmeofval  17445  nmfval  18107  nghmfval  18227  pcofval  18504  tchval  18646  ioombl  18918  ibladdlem  19170  itgaddlem1  19173  iblabs  19179  limccnp2  19238  dvbsss  19248  perfdvf  19249  evlval  19404  evl1fval  19406  mdegfval  19444  deg1fval  19462  deg1fvi  19467  uc1pval  19521  mon1pval  19523  avril1  20830  ismgm  20981  vafval  21153  bafval  21154  smfval  21155  vsfval  21185  bcsiALT  21754  dfrdg3  23557  trpredlem1  23634  bdayelon  23737  unisnif  23874  funpartfv  23893  fullfunfv  23895  axcontlem12  24013  linedegen  24176  elioo1t3  24913  oisbmi  24914  oisbmj  24915  oibbi1  24920  oibbi2  24921  intvconlem1  25114  hdrmp  25117  domval  25134  codval  25135  idval  25136  cmpval  25137  isconc2  25418  xsyysx  25556  bsstrs  25557  mzpmfp  26236  dsmmval2  26613  itgocn  26780  psgnfval  26834  mdetfval  26898  mendbas  26903  mendplusgfval  26904  mendmulrfval  26906  mendsca  26908  mendvscafval  26909  addcomgi  27072  ndmaovcl  27454  a9e2ndeq  27608  2sb5ndVD  27966  2sb5ndALT  27989  bnj1189  28318  ax12-2  28382  a12lem1  28409  a12study11  28417  a12study11n  28418  ax9vax9  28437
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator