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

Theorem pm2.61i 176
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 (𝜑𝜓)
pm2.61i.2 𝜑𝜓)
Assertion
Ref Expression
pm2.61i 𝜓

Proof of Theorem pm2.61i
StepHypRef Expression
1 id 22 . 2 (𝜑𝜑)
2 pm2.61i.2 . . 3 𝜑𝜓)
3 pm2.61i.1 . . 3 (𝜑𝜓)
42, 3ja 173 . 2 ((𝜑𝜑) → 𝜓)
51, 4ax-mp 5 1 𝜓
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem is referenced by:  pm2.61ii  177  pm2.61nii  178  pm2.61iii  179  pm2.65i  185  pm5.21nii  368  pm5.18  371  biass  374  pm2.61ian  830  ecase3  981  4cases  989  pm4.42  1003  ifpid  1024  elimh  1029  elimhOLD  1032  3ecase  1434  ax6e  2249  ax12  2303  exdistrf  2332  ax12OLD  2340  equvini  2345  dfsb2  2372  sbequi  2374  sbi1  2391  sbcom3  2410  sbco2  2414  sbco3  2416  sb9  2425  ax12vALT  2427  hbs1  2435  nfsb  2439  2ax6e  2449  sbal  2461  eujustALT  2472  pm2.61ine  2873  ralcom2  3098  eueq2  3367  moeq3  3370  mo2icl  3372  sbc2or  3431  sbcimdvOLD  3486  unineq  3859  csb0  3960  sbcel12  3961  sbcne12  3964  sbcel2  3967  csbidm  3980  csbun  3987  csbin  3988  ralidm  4053  ifsb  4077  ifid  4103  ifnot  4111  ifan  4112  ifor  4113  csbif  4116  elimhyp  4124  elimhyp2v  4125  elimhyp3v  4126  elimhyp4v  4127  elimdhyp  4129  keephyp2v  4131  keephyp3v  4132  eqoreldifOLD  4204  rabsnif  4235  tppreqb  4312  ssunsn2  4334  n0snor2el  4339  elpreqprlem  4370  dfopif  4374  csbuni  4439  sbcbr  4677  unisn2  4764  intabs  4795  class2set  4802  snexALT  4822  dtru  4827  dtruALT  4870  snex  4879  dtruALT2  4882  copsexg  4926  csbopab  4978  dfid3  5000  csbxp  5171  csbres  5369  csbima12  5452  soirri  5491  csbrn  5565  dmsnopss  5576  dmsnsnsn  5582  opswap  5591  unixpid  5639  nsuceq0  5774  ordsssuc2  5783  iotassuni  5836  iotaex  5837  dfiota4OLD  5849  csbiota  5850  dffv3  6154  fvrn0  6183  ndmfv  6185  elfv2ex  6196  fveqres  6197  csbfv12  6198  csbfv  6200  dffv2  6238  fvco4i  6243  fvmptss  6259  fvmptex  6261  fvmptss2  6270  f0cli  6336  fvunsn  6410  fconst5  6436  csbriota  6588  riotassuni  6613  csbov123  6652  csbov  6653  fvmptopab  6662  0neqopab  6663  brfvopab  6665  elimdelov  6701  ovif12  6704  ndmovcl  6784  ndmovord  6789  elovmpt3imp  6855  difsnexi  6934  ordsuc  6976  ordsucelsuc  6984  1stval  7130  2ndval  7131  1st2val  7154  2nd2val  7155  el2mpt2csbcl  7210  bropopvvv  7215  bropfvvvvlem  7216  bropfvvvv  7217  suppimacnv  7266  suppssdm  7268  ressuppss  7274  suppun  7275  extmptsuppeq  7279  funsssuppss  7281  fczsupp0  7284  suppss  7285  suppssov1  7287  suppss2  7289  suppssfv  7291  supp0cosupp0  7294  imacosupp  7295  mpt2xopynvov0  7304  mpt2xopoveqd  7307  pwuninel  7361  smofvon2  7413  om0x  7559  brdomg  7925  snfi  7998  sdomirr  8057  domunsn  8070  2pwuninel  8075  snnen2o  8109  suppeqfsuppbi  8249  fsuppun  8254  funsnfsupp  8259  fipwuni  8292  oicl  8394  oif  8395  wemapso2  8418  card2on  8419  en2lp  8470  tctr  8576  r1tr  8599  rankdmr1  8624  r1pw  8668  r1pwALT  8669  rankuni  8686  scottex  8708  cardidm  8745  alephcard  8853  alephnbtwn  8854  cdacomen  8963  cfub  9031  cardcf  9034  cflecard  9035  cfle  9036  cflim2  9045  cfidm  9057  isf32lem9  9143  itunisuc  9201  itunitc1  9202  itunitc  9203  ituniiun  9204  axcc2lem  9218  alephreg  9364  pwcfsdom  9365  cfpwsdom  9366  axunndlem1  9377  axpownd  9383  tskmcl  9623  addcompi  9676  addasspi  9677  mulcompi  9678  mulasspi  9679  distrpi  9680  addnidpi  9683  nlt1pi  9688  addcompq  9732  addcomnq  9733  mulcompq  9734  mulcomnq  9735  adderpq  9738  mulerpq  9739  addassnq  9740  mulassnq  9741  distrnq  9743  genpass  9791  addcompr  9803  mulcompr  9805  distrpr  9810  ltexprlem7  9824  addcomsr  9868  addasssr  9869  mulcomsr  9870  mulasssr  9871  distrsr  9872  uzssz  11667  uzwo  11711  nn01to3  11741  xnn0xaddcl  12025  elixx3g  12146  iooid  12161  elfz2  12291  injresinjlem  12544  injresinj  12545  fleqceilz  12609  modifeq2int  12688  modfzo0difsn  12698  addmodlteq  12701  ltweuz  12716  fzofi  12729  fsuppmapnn0fiubex  12748  hashrabrsn  13117  hashrabsn01  13118  hashrabsn1  13119  elprchashprn2  13140  hashss  13153  hashsn01  13160  hash1snb  13163  hashgt12el  13166  hashgt12el2  13167  hashfzp1  13174  hash2pwpr  13212  hashge2el2dif  13216  ccatsymb  13321  swrd00  13372  swrd0  13388  swrdccatin1  13436  repswswrd  13484  0csh0  13492  cshwcl  13497  cshwidxmod  13502  repswcshw  13511  cshw1  13521  s3sndisj  13656  s3iunsndisj  13657  xptrrel  13669  trclfvcotrg  13707  relexpfld  13739  modfsummods  14471  pwm1geoser  14544  dvdsaddre2b  14972  gcdaddmlem  15188  prm23ge5  15463  pcmptcl  15538  prmgaplem5  15702  prmgaplem6  15703  cshwshash  15754  strfvss  15821  strfvi  15853  setsnid  15855  ressbas  15870  ressbasss  15872  resslem  15873  ress0  15874  ressress  15878  strle1  15913  0rest  16030  firest  16033  topnval  16035  xpsaddlem  16175  xpsvsca  16179  homffval  16290  comfffval  16298  oppchomfval  16314  oppcbas  16318  fullfunc  16506  fthfunc  16507  natfval  16546  fucbas  16560  fuchom  16561  arwval  16633  coafval  16654  xpcbas  16758  xpchomfval  16759  xpccofval  16762  lubfun  16920  glbfun  16933  oduval  17070  oduleval  17071  odumeet  17080  odujoin  17082  ipopos  17100  plusffval  17187  grpidval  17200  gsum0  17218  frmdplusg  17331  frmd0  17337  mgm2nsgrplem2  17346  mgm2nsgrplem3  17347  sgrp2rid2  17353  dfgrp2e  17388  grpinvfval  17400  grpinvfvi  17403  grpsubfval  17404  mulgfval  17482  mulgfvi  17485  cntrval  17692  oppgval  17717  oppgplusfval  17718  symgbas  17740  symgplusg  17749  psgnfval  17860  odfval  17892  oppglsm  17997  efgval  18070  mgpval  18432  mgpplusg  18433  ringidval  18443  opprval  18564  opprmulfval  18565  dvdsrval  18585  invrfval  18613  dvrfval  18624  staffval  18787  scaffval  18821  rlmval  19131  rlmsca2  19141  2idlval  19173  rrgval  19227  asclfval  19274  psrplusg  19321  psrmulr  19324  psrvscafval  19330  mplval  19368  mplcoe3  19406  evlval  19464  psr1val  19496  vr1val  19502  ply1val  19504  ply1basfvi  19551  ply1plusgfvi  19552  psr1sca2  19561  ply1sca2  19564  ply1ascl  19568  cply1mul  19604  gsummoncoe1  19614  evl1fval  19632  evl1fval1  19635  zrhval  19796  zlmlem  19805  zlmvsca  19810  chrval  19813  evpmss  19872  psgndiflemB  19886  ipffval  19933  thlbas  19980  thlle  19981  thloc  19983  pjfval  19990  dsmmval2  20020  mamufacex  20135  mavmulsolcl  20297  marrepfval  20306  marepvfval  20311  submafval  20325  mdetfval  20332  mdetfval1  20336  mdetunilem7  20364  mdetunilem8  20365  madufval  20383  minmar1fval  20392  mp2pm2mplem4  20554  toponsspwpw  20666  tgdif0  20736  indislem  20744  resstopn  20930  iocpnfordt  20959  icomnfordt  20960  hmeofval  21501  ussval  22003  nmfval  22333  nghmfval  22466  pcofval  22750  tchval  22957  ioombl  23273  ibladdlem  23526  itgaddlem1  23529  iblabs  23535  dvbsss  23606  perfdvf  23607  mdegfval  23760  deg1fval  23778  deg1fvi  23783  uc1pval  23837  mon1pval  23839  lgsqrmodndvds  25012  gausslemma2dlem1a  25024  2lgs  25066  ttglem  25690  axcontlem12  25789  vtxval  25812  iedgval  25813  usgr1v  26075  nbuhgr  26160  nbumgr  26164  uhgrnbgr0nb  26171  nbgr1vtx  26175  nbgrnself2  26180  nbusgrvtxm1  26202  uvtxa0  26215  sizusglecusg  26280  g0wlk0  26451  wlkreslem  26469  lfgrwlkprop  26487  wwlks  26630  wwlksn  26632  wspthsn  26638  iswwlksnon  26643  iswspthsnon  26644  0enwwlksnge1  26652  wwlksnfi  26704  wwlksnonfi  26719  wspn0  26723  wwlks2onv  26750  2wspdisj  26757  2wspiundisj  26758  clwwlks  26780  clwwlksn  26782  clwlkclwwlklem2a4  26799  umgrclwwlksge2  26812  clwwlksnfi  26813  1conngr  26954  eupth2lem3lem7  26994  frgr1v  27033  nfrgr2v  27034  1to2vfriswmgr  27041  frgrncvvdeqlem2  27062  2wspmdisj  27093  frgrreggt1  27139  frgrreg  27140  frgrregord013  27141  frgrogt3nreg  27143  friendship  27145  avril1  27207  vafval  27346  bafval  27347  smfval  27348  vsfval  27376  bcsiALT  27924  resvsca  29657  resvlem  29658  cntnevol  30114  signsw0glem  30452  bnj1189  30838  mvtval  31158  mexval  31160  mexval2  31161  mdvval  31162  mrsubfval  31166  mrsubrn  31171  msubfval  31182  elmsubrn  31186  msubrn  31187  mvhfval  31191  mpstval  31193  msrfval  31195  mstaval  31202  mppsval  31230  mthmval  31233  dfrdg3  31456  trpredlem1  31481  bdayelon  31596  fvsingle  31722  unisnif  31727  funpartfv  31747  fullfunfv  31749  linedegen  31945  bj-ax6e  32348  axc11n11r  32368  bj-ax12v3ALT  32371  bj-dtru  32493  bj-sbsb  32520  bj-nfcsym  32586  bj-restsnid  32730  bj-inftyexpidisj  32769  csbdif  32842  finxpreclem4  32902  finxp00  32910  wl-nfs1t  32995  wl-sbcom3  33043  matunitlindflem1  33076  itg2addnclem  33132  ibladdnclem  33137  itgaddnclem1  33139  iblabsnc  33145  iblmulc2nc  33146  ftc1anclem8  33163  ismgmOLD  33320  tsbi1  33611  tsbi2  33612  ac6s6  33651  equid1  33703  ax12fromc15  33709  equid1ALT  33729  dvelimf-o  33733  ax12inda2ALT  33750  ax12inda2  33751  mzpmfp  36829  itgocn  37254  mendbas  37274  mendplusgfval  37275  mendmulrfval  37277  mendsca  37279  mendvscafval  37280  arearect  37321  areaquad  37322  or3or  37840  uneqsn  37842  addcomgi  38181  ax6e2ndeq  38296  2sb5ndVD  38668  2sb5ndALT  38690  sqwvfoura  39782  sqwvfourb  39783  fourierswlem  39784  fouriersw  39785  hspdifhsp  40167  hspmbllem2  40178  hspmbl  40180  tz6.12-afv  40587  ndmaovcl  40617  otiunsndisjX  40625  nltle2tri  40650  fzopredsuc  40660  iccpartiltu  40686  iccpartigtl  40687  iccpartlt  40688  icceuelpartlem  40699  iccpartnel  40702  pfx00  40713  pfx0  40714  fmtnoprmfac1  40806  fmtnoprmfac2  40808  prmdvdsfmtnof1lem2  40826  prminf2  40829  lighneallem4  40856  evenprm2  40952  stgoldbwt  40989  upwlkbprop  41037  elsprel  41043  sprssspr  41049  sprsymrelfvlem  41058  nzerooringczr  41390  pgrpgt2nabl  41465  suppmptcfin  41478  linc1  41532  lindslinindsimp2lem5  41569  setrec2lem1  41763
  Copyright terms: Public domain W3C validator