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  dvelimh  1906  exdistrf  1913  equveli  1930  dfsb2  1997  sbn  2004  sbi1  2005  sbco2  2028  sbco3  2030  sb9i  2036  ax11v  2038  hbs1  2046  nfsb  2050  sbal1  2067  sbal  2068  dvelimALT  2074  ax11  2096  equid1  2099  equid1ALT  2117  dvelimf-o  2121  ax11inda2ALT  2139  ax11inda2  2140  eujustALT  2148  moexex  2214  pm2.61ne  2523  pm2.61ine  2524  rgen2a  2611  ralcom2  2706  eueq2  2941  moeq3  2944  mo2icl  2946  sbc2or  3001  unineq  3421  ralidm  3559  ifsb  3576  ifid  3599  ifnot  3605  ifan  3606  ifor  3607  elimhyp  3615  elimhyp2v  3616  elimhyp3v  3617  elimhyp4v  3618  elimdhyp  3620  keephyp2v  3622  keephyp3v  3623  ssunsn2  3775  dfopif  3795  intabs  4174  class2set  4180  snexALT  4198  dtru  4203  dtruALT  4209  snex  4218  dtruALT2  4221  copsexg  4254  dfid3  4312  nsuceq0  4474  ordsssuc2  4483  unisn2  4524  ordsuc  4607  ordsucelsuc  4615  soirri  5071  soirriOLD  5076  dmsnopss  5147  dmsnsnsn  5153  opswap  5161  unixpid  5209  iotassuni  5237  iotaex  5238  dfiota4  5249  dffv3  5523  fvrn0  5552  ndmfv  5554  fveqres  5562  dffv2  5594  fvco4i  5599  fvmptss  5611  fvmptex  5612  fvmptss2  5621  f0cli  5673  fvunsn  5714  fconst5  5733  elimdelov  5929  ndmovcl  6007  ndmovord  6012  1stval  6126  2ndval  6127  1st2val  6147  2nd2val  6148  pwuninel  6302  riotav  6311  riotassuni  6345  smofvon2  6375  om0x  6520  brdomg  6874  snfi  6943  sdomirr  7000  domunsn  7013  2pwuninel  7018  fipwuni  7181  oicl  7246  oif  7247  card2on  7270  en2lp  7319  tctr  7427  r1tr  7450  rankdmr1  7475  r1pw  7519  r1pwOLD  7520  rankuni  7537  scottex  7557  cardidm  7594  alephcard  7699  alephnbtwn  7700  cdacomen  7809  cfub  7877  cardcf  7880  cflecard  7881  cfle  7882  cflim2  7891  cfidm  7903  isf32lem9  7989  itunisuc  8047  itunitc1  8048  itunitc  8049  ituniiun  8050  axcc2lem  8064  alephreg  8206  pwcfsdom  8207  cfpwsdom  8208  axunndlem1  8219  axpownd  8225  tskmcl  8465  addcompi  8520  addasspi  8521  mulcompi  8522  mulasspi  8523  distrpi  8524  addnidpi  8527  nlt1pi  8532  addcompq  8576  addcomnq  8577  mulcompq  8578  mulcomnq  8579  adderpq  8582  mulerpq  8583  addassnq  8584  mulassnq  8585  distrnq  8587  genpass  8635  addcompr  8647  mulcompr  8649  distrpr  8654  ltexprlem7  8668  addcomsr  8711  addasssr  8712  mulcomsr  8713  mulasssr  8714  distrsr  8715  uzssz  10249  uzwo  10283  uzwoOLD  10284  elixx3g  10671  iooid  10686  elfz2  10791  ltweuz  11026  fzofi  11038  hashsnlei  11378  swrd00  11453  gcdaddmlem  12709  pcmptcl  12941  strfvss  13168  strfvi  13188  setsnid  13190  ressbas  13200  ressbasss  13202  resslem  13203  ress0  13204  ressress  13207  strle1  13241  0rest  13336  firest  13339  topnval  13341  xpsaddlem  13479  xpsvsca  13483  homffval  13596  comfffval  13603  oppchomfval  13619  oppcbas  13623  fullfunc  13782  fthfunc  13783  natfval  13822  fucbas  13836  fuchom  13837  arwval  13877  coafval  13898  xpcbas  13954  xpchomfval  13955  xpccofval  13958  oduval  14236  oduleval  14237  odumeet  14246  odujoin  14248  ipopos  14265  plusffval  14381  grpidval  14386  gsum0  14459  frmdplusg  14478  frmd0  14484  grpinvfval  14522  grpinvfvi  14525  grpsubfval  14526  mulgfval  14570  mulgfvi  14573  symgbas  14774  symgplusg  14778  cntrval  14797  oppgval  14822  oppgplusfval  14823  odfval  14850  oppglsm  14955  efgval  15028  mgpval  15330  mgpplusg  15331  rngidval  15345  opprval  15408  opprmulfval  15409  dvdsrval  15429  invrfval  15457  dvrfval  15468  staffval  15614  scaffval  15647  rlmval  15947  rlmsca2  15955  2idlval  15987  rrgval  16030  asclfval  16076  psrplusg  16128  psrmulr  16131  psrvscafval  16137  mplval  16175  mplcoe3  16212  psr1val  16267  vr1val  16273  ply1val  16275  ply1basfvi  16321  ply1plusgfvi  16322  psr1sca2  16331  ply1sca2  16334  ply1ascl  16337  zrhval  16464  zlmlem  16473  zlmvsca  16478  chrval  16481  ipffval  16554  thlbas  16598  thlle  16599  thloc  16601  pjfval  16608  tgdif0  16732  indislem  16739  resstopn  16918  iocpnfordt  16947  icomnfordt  16948  hmeofval  17451  nmfval  18113  nghmfval  18233  pcofval  18510  tchval  18652  ioombl  18924  ibladdlem  19176  itgaddlem1  19179  iblabs  19185  limccnp2  19244  dvbsss  19254  perfdvf  19255  evlval  19410  evl1fval  19412  mdegfval  19450  deg1fval  19468  deg1fvi  19473  uc1pval  19527  mon1pval  19529  avril1  20838  ismgm  20989  vafval  21161  bafval  21162  smfval  21163  vsfval  21193  bcsiALT  21760  cntnevol  23177  dfrdg3  24155  trpredlem1  24232  bdayelon  24336  unisnif  24466  funpartfv  24485  fullfunfv  24487  axcontlem12  24605  linedegen  24768  itg2addnclem  24933  elioo1t3  25513  oisbmi  25514  oisbmj  25515  oibbi1  25520  oibbi2  25521  intvconlem1  25714  hdrmp  25717  domval  25734  codval  25735  idval  25736  cmpval  25737  isconc2  26018  xsyysx  26156  bsstrs  26157  mzpmfp  26836  dsmmval2  27213  itgocn  27380  psgnfval  27434  mdetfval  27498  mendbas  27503  mendplusgfval  27504  mendmulrfval  27506  mendsca  27508  mendvscafval  27509  addcomgi  27672  ndmaovcl  28074  mpt2xopynvov0  28095  mpt2xopoveqd  28098  elprchashprn2  28099  usgraedgprv  28133  usgra1v  28137  nbusgra  28154  nbgra0nb  28155  nbgranself2  28162  cusgra1v  28168  uvtxisvtx  28173  uvtx0  28174  uvtx01vtx  28175  frgra2v  28188  1to2vfriswmgra  28195  a9e2ndeq  28381  2sb5ndVD  28759  2sb5ndALT  28782  bnj1189  29112  ax12-2  29176  a12lem1  29203  a12study11  29211  a12study11n  29212  ax9vax9  29231
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator