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  367  pm5.18  370  biass  373  pm2.61ian  848  ecase3  1001  4cases  1009  pm4.42  1024  ifpid  1045  elimh  1050  3ecase  1477  ax6e  2286  ax12  2340  exdistrf  2364  ax12OLD  2372  equvini  2374  dfsb2  2401  sbequi  2403  sbi1  2420  sbcom3  2439  sbco2  2443  sbco3  2445  sb9  2454  ax12vALT  2456  hbs1  2464  nfsb  2468  2ax6e  2478  sbal  2490  eujustALT  2501  pm2.61ine  2906  ralcom2  3133  eueq2  3413  moeq3  3416  mo2icl  3418  sbc2or  3477  sbcimdvOLD  3532  unineq  3910  csb0  4015  sbcel12  4016  sbcne12  4019  sbcel2  4022  csbidm  4035  csbun  4042  csbin  4043  ralidm  4108  ifsb  4132  ifid  4158  ifnot  4166  ifan  4167  ifor  4168  csbif  4171  elimhyp  4179  elimhyp2v  4180  elimhyp3v  4181  elimhyp4v  4182  elimdhyp  4184  keephyp2v  4186  keephyp3v  4187  eqoreldifOLD  4258  rabsnif  4290  tppreqb  4368  ssunsn2  4391  n0snor2el  4396  elpreqprlem  4426  dfopif  4430  csbuni  4498  disjord  4673  sbcbr  4740  unisn2  4827  intabs  4855  class2set  4862  snexALT  4882  dtru  4887  dtruALT  4929  snex  4938  dtruALT2  4941  copsexg  4985  csbopab  5037  dfid3  5054  csbxp  5234  csbres  5431  csbima12  5518  soirri  5557  csbrn  5631  dmsnopss  5643  dmsnsnsn  5649  opswap  5660  unixpid  5708  nsuceq0  5843  ordsssuc2  5852  iotassuni  5905  iotaex  5906  dfiota4OLD  5918  csbiota  5919  dffv3  6225  fvrn0  6254  ndmfv  6256  elfv2ex  6267  fveqres  6268  csbfv12  6269  csbfv  6271  dffv2  6310  fvco4i  6315  fvmptss  6331  fvmptex  6333  fvmptss2  6343  fvmptrabfv  6348  f0cli  6410  fvunsn  6486  fconst5  6512  csbriota  6663  riotassuni  6688  csbov123  6727  csbov  6728  fvmptopab  6739  0neqopab  6740  brfvopab  6742  elimdelov  6778  ovif12  6781  ndmovcl  6861  ndmovord  6866  elovmpt3imp  6932  difsnexi  7012  ordsuc  7056  ordsucelsuc  7064  1stval  7212  2ndval  7213  1st2val  7238  2nd2val  7239  el2mpt2csbcl  7295  bropopvvv  7300  bropfvvvvlem  7301  bropfvvvv  7302  suppimacnv  7351  suppssdm  7353  ressuppss  7359  suppun  7360  extmptsuppeq  7364  funsssuppss  7366  fczsupp0  7369  suppss  7370  suppssov1  7372  suppss2  7374  suppssfv  7376  supp0cosupp0  7379  imacosupp  7380  mpt2xopynvov0  7389  mpt2xopoveqd  7392  pwuninel  7446  smofvon2  7498  om0x  7644  brdomg  8007  snfi  8079  sdomirr  8138  domunsn  8151  2pwuninel  8156  snnen2o  8190  suppeqfsuppbi  8330  fsuppun  8335  funsnfsupp  8340  fipwuni  8373  oicl  8475  oif  8476  wemapso2  8499  card2on  8500  en2lp  8548  tctr  8654  r1tr  8677  rankdmr1  8702  r1pw  8746  r1pwALT  8747  rankuni  8764  scottex  8786  cardidm  8823  alephcard  8931  alephnbtwn  8932  cdacomen  9041  cfub  9109  cardcf  9112  cflecard  9113  cfle  9114  cflim2  9123  cfidm  9135  isf32lem9  9221  itunisuc  9279  itunitc1  9280  itunitc  9281  ituniiun  9282  axcc2lem  9296  alephreg  9442  pwcfsdom  9443  cfpwsdom  9444  axunndlem1  9455  axpownd  9461  tskmcl  9701  addcompi  9754  addasspi  9755  mulcompi  9756  mulasspi  9757  distrpi  9758  addnidpi  9761  nlt1pi  9766  addcompq  9810  addcomnq  9811  mulcompq  9812  mulcomnq  9813  adderpq  9816  mulerpq  9817  addassnq  9818  mulassnq  9819  distrnq  9821  genpass  9869  addcompr  9881  mulcompr  9883  distrpr  9888  ltexprlem7  9902  addcomsr  9946  addasssr  9947  mulcomsr  9948  mulasssr  9949  distrsr  9950  uzssz  11745  uzwo  11789  nn01to3  11819  xnn0xaddcl  12104  elixx3g  12226  iooid  12241  elfz2  12371  injresinjlem  12628  injresinj  12629  fleqceilz  12693  modifeq2int  12772  modfzo0difsn  12782  addmodlteq  12785  ltweuz  12800  fzofi  12813  fsuppmapnn0fiubex  12832  hashrabrsn  13199  hashrabsn01  13200  hashrabsn1  13201  elprchashprn2  13222  hashss  13235  hashsn01  13242  hash1snb  13245  hashgt12el  13248  hashgt12el2  13249  hashfzp1  13256  hash2pwpr  13296  hashge2el2dif  13300  ccatsymb  13400  swrd00  13463  swrd0  13480  swrdccatin1  13529  repswswrd  13577  0csh0  13585  cshwcl  13590  cshwidxmod  13595  repswcshw  13604  cshw1  13614  s3sndisj  13752  s3iunsndisj  13753  xptrrel  13765  trclfvcotrg  13801  relexpfld  13833  modfsummods  14569  pwm1geoser  14644  dvdsaddre2b  15076  gcdaddmlem  15292  prm23ge5  15567  pcmptcl  15642  prmgaplem5  15806  prmgaplem6  15807  cshwshash  15858  strfvss  15927  strfvi  15960  setsnid  15962  ressbas  15977  ressbasss  15979  resslem  15980  ress0  15981  ressress  15985  strle1  16020  0rest  16137  firest  16140  topnval  16142  xpsaddlem  16282  xpsvsca  16286  homffval  16397  comfffval  16405  oppchomfval  16421  oppcbas  16425  fullfunc  16613  fthfunc  16614  natfval  16653  fucbas  16667  fuchom  16668  arwval  16740  coafval  16761  xpcbas  16865  xpchomfval  16866  xpccofval  16869  lubfun  17027  glbfun  17040  oduval  17177  oduleval  17178  odumeet  17187  odujoin  17189  ipopos  17207  plusffval  17294  grpidval  17307  gsum0  17325  frmdplusg  17438  frmd0  17444  mgm2nsgrplem2  17453  mgm2nsgrplem3  17454  sgrp2rid2  17460  dfgrp2e  17495  grpinvfval  17507  grpinvfvi  17510  grpsubfval  17511  mulgfval  17589  mulgfvi  17592  cntrval  17798  oppgval  17823  oppgplusfval  17824  symgbas  17846  symgplusg  17855  psgnfval  17966  odfval  17998  oppglsm  18103  efgval  18176  mgpval  18538  mgpplusg  18539  ringidval  18549  opprval  18670  opprmulfval  18671  dvdsrval  18691  invrfval  18719  dvrfval  18730  staffval  18895  scaffval  18929  rlmval  19239  rlmsca2  19249  2idlval  19281  rrgval  19335  asclfval  19382  psrplusg  19429  psrmulr  19432  psrvscafval  19438  mplval  19476  mplcoe3  19514  evlval  19572  psr1val  19604  vr1val  19610  ply1val  19612  ply1basfvi  19659  ply1plusgfvi  19660  psr1sca2  19669  ply1sca2  19672  ply1ascl  19676  cply1mul  19712  gsummoncoe1  19722  evl1fval  19740  evl1fval1  19743  zrhval  19904  zlmlem  19913  zlmvsca  19918  chrval  19921  evpmss  19980  psgndiflemB  19994  ipffval  20041  thlbas  20088  thlle  20089  thloc  20091  pjfval  20098  dsmmval2  20128  mamufacex  20243  mavmulsolcl  20405  marrepfval  20414  marepvfval  20419  submafval  20433  mdetfval  20440  mdetfval1  20444  mdetunilem7  20472  mdetunilem8  20473  madufval  20491  minmar1fval  20500  mp2pm2mplem4  20662  toponsspwpw  20774  tgdif0  20844  indislem  20852  resstopn  21038  iocpnfordt  21067  icomnfordt  21068  hmeofval  21609  ussval  22110  nmfval  22440  nghmfval  22573  pcofval  22856  tchval  23063  ioombl  23379  ibladdlem  23631  itgaddlem1  23634  iblabs  23640  dvbsss  23711  perfdvf  23712  mdegfval  23867  deg1fval  23885  deg1fvi  23890  uc1pval  23944  mon1pval  23946  lgsqrmodndvds  25123  gausslemma2dlem1a  25135  2lgs  25177  ttglem  25801  axcontlem12  25900  vtxval  25923  iedgval  25924  edgval  25986  usgr1v  26193  nbuhgr  26284  nbumgr  26288  uhgrnbgr0nb  26295  nbgr1vtx  26299  nbgrnself2  26301  nbgrnself2OLD  26304  nbusgrvtxm1  26325  sizusglecusg  26415  g0wlk0  26604  wlkreslem  26622  lfgrwlkprop  26640  wwlks  26783  wwlksn  26785  wspthsn  26797  iswwlksnon  26802  iswwlksnonOLD  26803  iswspthsnon  26806  iswspthsnonOLD  26807  0enwwlksnge1  26818  wwlksnfi  26869  clwwlk  26951  umgrclwwlkge2  26957  clwlkclwwlklem2a4  26963  clwwlkn  26985  clwwlknOLD  26986  clwwlknfi  27008  clwwlknonmpt2  27062  clwwlknon  27063  clwwlk0on0  27067  clwwlknon1le1  27076  1conngr  27172  eupth2lem3lem7  27212  frgr1v  27251  nfrgr2v  27252  1to2vfriswmgr  27259  2wspmdisj  27317  frgrreggt1  27380  frgrreg  27381  frgrregord013  27382  frgrogt3nreg  27384  friendship  27386  avril1  27449  vafval  27586  bafval  27587  smfval  27588  vsfval  27616  bcsiALT  28164  resvsca  29958  resvlem  29959  cntnevol  30419  signsw0glem  30758  bnj1189  31203  mvtval  31523  mexval  31525  mexval2  31526  mdvval  31527  mrsubfval  31531  mrsubrn  31536  msubfval  31547  elmsubrn  31551  msubrn  31552  mvhfval  31556  mpstval  31558  msrfval  31560  mstaval  31567  mppsval  31595  mthmval  31598  dfrdg3  31826  trpredlem1  31851  fvsingle  32152  unisnif  32157  funpartfv  32177  fullfunfv  32179  linedegen  32375  bj-ax6e  32778  axc11n11r  32798  bj-ax12v3ALT  32801  bj-dtru  32922  bj-sbsb  32949  bj-nfcsym  33011  bj-restsnid  33165  bj-inftyexpidisj  33227  csbdif  33301  finxpreclem4  33361  finxp00  33369  wl-nfs1t  33454  wl-sbcom3  33502  matunitlindflem1  33535  itg2addnclem  33591  ibladdnclem  33596  itgaddnclem1  33598  iblabsnc  33604  iblmulc2nc  33605  ftc1anclem8  33622  ismgmOLD  33779  tsbi1  34070  tsbi2  34071  ac6s6  34110  equid1  34503  ax12fromc15  34509  equid1ALT  34529  dvelimf-o  34533  ax12inda2ALT  34550  ax12inda2  34551  mzpmfp  37627  itgocn  38051  mendbas  38071  mendplusgfval  38072  mendmulrfval  38074  mendsca  38076  mendvscafval  38077  arearect  38118  areaquad  38119  or3or  38636  uneqsn  38638  addcomgi  38977  ax6e2ndeq  39092  2sb5ndVD  39460  2sb5ndALT  39482  sqwvfoura  40763  sqwvfourb  40764  fourierswlem  40765  fouriersw  40766  hspdifhsp  41151  hspmbllem2  41162  hspmbl  41164  tz6.12-afv  41574  ndmaovcl  41604  otiunsndisjX  41621  fvmptrab  41631  nltle2tri  41648  fzopredsuc  41658  iccpartiltu  41683  iccpartigtl  41684  iccpartlt  41685  icceuelpartlem  41696  iccpartnel  41699  pfx00  41709  pfx0  41710  fmtnoprmfac1  41802  fmtnoprmfac2  41804  prmdvdsfmtnof1lem2  41822  prminf2  41825  lighneallem4  41852  evenprm2  41948  even3prm2  41953  stgoldbwt  41989  upwlkbprop  42044  elsprel  42050  sprssspr  42056  sprsymrelfvlem  42065  nzerooringczr  42397  pgrpgt2nabl  42472  suppmptcfin  42485  linc1  42539  lindslinindsimp2lem5  42576  setrec2lem1  42765
  Copyright terms: Public domain W3C validator