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  866  ecase3  1019  4cases  1027  pm4.42  1042  ifpid  1063  elimh  1068  3ecase  1582  ax6e  2391  ax12  2445  exdistrf  2469  ax12OLD  2477  equvini  2479  dfsb2  2506  sbequi  2508  sbi1  2525  sbcom3  2544  sbco2  2548  sbco3  2550  sb9  2559  ax12vALT  2561  hbs1  2569  nfsb  2573  2ax6e  2583  sbal  2595  eujustALT  2606  pm2.61ine  3011  ralcom2  3238  eueq2  3517  moeq3  3520  mo2icl  3522  sbc2or  3581  sbcimdvOLD  3636  unineq  4016  csb0  4121  sbcel12  4122  sbcne12  4125  sbcel2  4128  csbidm  4141  csbun  4148  csbin  4149  ralidm  4215  ifsb  4239  ifid  4265  ifnot  4273  ifan  4274  ifor  4275  csbif  4278  elimhyp  4286  elimhyp2v  4287  elimhyp3v  4288  elimhyp4v  4289  elimdhyp  4291  keephyp2v  4293  keephyp3v  4294  eqoreldifOLD  4366  rabsnif  4398  tppreqb  4477  ssunsn2  4500  n0snor2el  4505  preq12nebg  4539  opthprneg  4541  elpreqprlem  4542  dfopif  4546  csbuni  4614  disjord  4789  sbcbr  4855  unisn2  4942  intabs  4970  class2set  4977  snexALT  4997  dtru  5002  dtruALT  5044  snex  5053  dtruALT2  5056  copsexg  5100  csbopab  5154  dfid3  5171  csbxp  5353  csbres  5550  csbima12  5637  soirri  5676  csbrn  5750  dmsnopss  5762  dmsnsnsn  5768  opswap  5779  unixpid  5827  nsuceq0  5962  ordsssuc2  5971  iotassuni  6024  iotaex  6025  dfiota4OLD  6037  csbiota  6038  dffv3  6344  fvrn0  6373  ndmfv  6375  elfv2ex  6386  fveqres  6387  csbfv12  6388  csbfv  6390  dffv2  6429  fvco4i  6434  fvmptss  6450  fvmptex  6452  fvmptss2  6462  fvmptrabfv  6467  f0cli  6529  fvunsn  6605  fconst5  6631  csbriota  6782  riotassuni  6807  csbov123  6846  csbov  6847  fvmptopab  6858  0neqopab  6859  brfvopab  6861  elimdelov  6897  ovif12  6900  ndmovcl  6980  ndmovord  6985  elovmpt3imp  7051  difsnexi  7131  ordsuc  7175  ordsucelsuc  7183  1stval  7331  2ndval  7332  1st2val  7357  2nd2val  7358  el2mpt2csbcl  7414  bropopvvv  7419  bropfvvvvlem  7420  bropfvvvv  7421  suppimacnv  7470  suppssdm  7472  ressuppss  7478  suppun  7479  extmptsuppeq  7483  funsssuppss  7486  fczsupp0  7489  suppss  7490  suppssov1  7492  suppss2  7494  suppssfv  7496  supp0cosupp0  7499  imacosupp  7500  mpt2xopynvov0  7509  mpt2xopoveqd  7512  pwuninel  7566  smofvon2  7618  om0x  7764  brdomg  8127  snfi  8199  sdomirr  8258  domunsn  8271  2pwuninel  8276  snnen2o  8310  suppeqfsuppbi  8450  fsuppun  8455  funsnfsupp  8460  fipwuni  8493  oicl  8595  oif  8596  wemapso2  8619  card2on  8620  en2lp  8671  tctr  8785  r1tr  8808  rankdmr1  8833  r1pw  8877  r1pwALT  8878  rankuni  8895  scottex  8917  cardidm  8971  alephcard  9079  alephnbtwn  9080  cdacomen  9191  cfub  9259  cardcf  9262  cflecard  9263  cfle  9264  cflim2  9273  cfidm  9285  isf32lem9  9371  itunisuc  9429  itunitc1  9430  itunitc  9431  ituniiun  9432  axcc2lem  9446  alephreg  9592  pwcfsdom  9593  cfpwsdom  9594  axunndlem1  9605  axpownd  9611  tskmcl  9851  addcompi  9904  addasspi  9905  mulcompi  9906  mulasspi  9907  distrpi  9908  addnidpi  9911  nlt1pi  9916  addcompq  9960  addcomnq  9961  mulcompq  9962  mulcomnq  9963  adderpq  9966  mulerpq  9967  addassnq  9968  mulassnq  9969  distrnq  9971  genpass  10019  addcompr  10031  mulcompr  10033  distrpr  10038  ltexprlem7  10052  addcomsr  10096  addasssr  10097  mulcomsr  10098  mulasssr  10099  distrsr  10100  uzssz  11895  uzwo  11940  nn01to3  11970  xnn0xaddcl  12255  elixx3g  12377  iooid  12392  elfz2  12522  injresinjlem  12778  injresinj  12779  fleqceilz  12843  modifeq2int  12922  modfzo0difsn  12932  addmodlteq  12935  ltweuz  12950  fzofi  12963  fsuppmapnn0fiubex  12982  hashrabrsn  13349  hashrabsn01  13350  hashrabsn1  13351  elprchashprn2  13372  hashss  13385  hashsn01  13392  hash1snb  13395  hashgt12el  13398  hashgt12el2  13399  hashfzp1  13406  hash2pwpr  13446  hashge2el2dif  13450  ccatsymb  13550  swrd00  13613  swrd0  13630  swrdccatin1  13679  repswswrd  13727  0csh0  13735  cshwcl  13740  cshwidxmod  13745  repswcshw  13754  cshw1  13764  s3sndisj  13903  s3iunsndisj  13904  xptrrel  13916  trclfvcotrg  13952  relexpfld  13984  modfsummods  14720  pwm1geoser  14795  dvdsaddre2b  15227  gcdaddmlem  15443  prm23ge5  15718  pcmptcl  15793  prmgaplem5  15957  prmgaplem6  15958  cshwshash  16009  strfvss  16078  strfvi  16111  setsnid  16113  ressbas  16128  ressbasss  16130  resslem  16131  ress0  16132  ressress  16136  strle1  16171  0rest  16288  firest  16291  topnval  16293  xpsaddlem  16433  xpsvsca  16437  homffval  16547  comfffval  16555  oppchomfval  16571  oppcbas  16575  fullfunc  16763  fthfunc  16764  natfval  16803  fucbas  16817  fuchom  16818  arwval  16890  coafval  16911  xpcbas  17015  xpchomfval  17016  xpccofval  17019  lubfun  17177  glbfun  17190  oduval  17327  oduleval  17328  odumeet  17337  odujoin  17339  ipopos  17357  plusffval  17444  grpidval  17457  gsum0  17475  frmdplusg  17588  frmd0  17594  mgm2nsgrplem2  17603  mgm2nsgrplem3  17604  sgrp2rid2  17610  dfgrp2e  17645  grpinvfval  17657  grpinvfvi  17660  grpsubfval  17661  mulgfval  17739  mulgfvi  17742  cntrval  17948  oppgval  17973  oppgplusfval  17974  symgbas  17996  symgplusg  18005  psgnfval  18116  odfval  18148  oppglsm  18253  efgval  18326  mgpval  18688  mgpplusg  18689  ringidval  18699  opprval  18820  opprmulfval  18821  dvdsrval  18841  invrfval  18869  dvrfval  18880  staffval  19045  scaffval  19079  rlmval  19389  rlmsca2  19399  2idlval  19431  rrgval  19485  asclfval  19532  psrplusg  19579  psrmulr  19582  psrvscafval  19588  mplval  19626  mplcoe3  19664  evlval  19722  psr1val  19754  vr1val  19760  ply1val  19762  ply1basfvi  19809  ply1plusgfvi  19810  psr1sca2  19819  ply1sca2  19822  ply1ascl  19826  cply1mul  19862  gsummoncoe1  19872  evl1fval  19890  evl1fval1  19893  zrhval  20054  zlmlem  20063  zlmvsca  20068  chrval  20071  evpmss  20130  psgndiflemB  20144  ipffval  20191  thlbas  20238  thlle  20239  thloc  20241  pjfval  20248  dsmmval2  20278  mamufacex  20393  mavmulsolcl  20555  marrepfval  20564  marepvfval  20569  submafval  20583  mdetfval  20590  mdetfval1  20594  mdetunilem7  20622  mdetunilem8  20623  madufval  20641  minmar1fval  20650  mp2pm2mplem4  20812  toponsspwpw  20924  tgdif0  20994  indislem  21002  resstopn  21188  iocpnfordt  21217  icomnfordt  21218  hmeofval  21759  ussval  22260  nmfval  22590  nghmfval  22723  pcofval  23006  tchval  23213  ioombl  23529  ibladdlem  23781  itgaddlem1  23784  iblabs  23790  dvbsss  23861  perfdvf  23862  mdegfval  24017  deg1fval  24035  deg1fvi  24040  uc1pval  24094  mon1pval  24096  lgsqrmodndvds  25273  gausslemma2dlem1a  25285  2lgs  25327  ttglem  25951  axcontlem12  26050  vtxval  26073  iedgval  26074  edgval  26136  usgr1v  26343  nbuhgr  26434  nbumgr  26438  uhgrnbgr0nb  26445  nbgr1vtx  26449  nbgrnself2  26451  nbgrnself2OLD  26454  nbusgrvtxm1  26475  sizusglecusg  26565  g0wlk0  26754  wlkreslem  26772  lfgrwlkprop  26790  wwlks  26934  wwlksn  26936  wspthsn  26948  iswwlksnon  26953  iswwlksnonOLD  26954  iswspthsnon  26957  iswspthsnonOLD  26958  0enwwlksnge1  26969  wwlksnfi  27020  clwwlk  27102  umgrclwwlkge2  27110  clwlkclwwlklem2a4  27116  clwwlkn  27147  clwwlknOLD  27148  clwwlknfi  27170  clwwlknonmpt2  27230  clwwlknon  27231  clwwlk0on0  27235  clwwlknon1le1  27245  1conngr  27342  eupth2lem3lem7  27382  frgr1v  27421  nfrgr2v  27422  1to2vfriswmgr  27429  2wspmdisj  27487  frgrreggt1  27557  frgrreg  27558  frgrregord013  27559  frgrogt3nreg  27561  friendship  27563  avril1  27626  vafval  27763  bafval  27764  smfval  27765  vsfval  27793  bcsiALT  28341  resvsca  30135  resvlem  30136  cntnevol  30596  signsw0glem  30935  bnj1189  31380  mvtval  31700  mexval  31702  mexval2  31703  mdvval  31704  mrsubfval  31708  mrsubrn  31713  msubfval  31724  elmsubrn  31728  msubrn  31729  mvhfval  31733  mpstval  31735  msrfval  31737  mstaval  31744  mppsval  31772  mthmval  31775  dfrdg3  32003  trpredlem1  32028  fvsingle  32329  unisnif  32334  funpartfv  32354  fullfunfv  32356  linedegen  32552  bj-ax6e  32955  axc11n11r  32975  bj-ax12v3ALT  32978  bj-dtru  33099  bj-sbsb  33126  bj-nfcsym  33188  bj-restsnid  33342  bj-inftyexpidisj  33404  csbdif  33478  finxpreclem4  33538  finxp00  33546  wl-nfs1t  33633  wl-sbcom3  33681  matunitlindflem1  33714  itg2addnclem  33770  ibladdnclem  33775  itgaddnclem1  33777  iblabsnc  33783  iblmulc2nc  33784  ftc1anclem8  33801  ismgmOLD  33958  tsbi1  34249  tsbi2  34250  ac6s6  34289  equid1  34684  ax12fromc15  34690  equid1ALT  34710  dvelimf-o  34714  ax12inda2ALT  34731  ax12inda2  34732  mzpmfp  37808  itgocn  38232  mendbas  38252  mendplusgfval  38253  mendmulrfval  38255  mendsca  38257  mendvscafval  38258  arearect  38299  areaquad  38300  or3or  38817  uneqsn  38819  addcomgi  39158  ax6e2ndeq  39273  2sb5ndVD  39641  2sb5ndALT  39663  sqwvfoura  40944  sqwvfourb  40945  fourierswlem  40946  fouriersw  40947  hspdifhsp  41332  hspmbllem2  41343  hspmbl  41345  tz6.12-afv  41755  ndmaovcl  41785  otiunsndisjX  41802  fvmptrab  41812  nltle2tri  41829  fzopredsuc  41839  iccpartiltu  41864  iccpartigtl  41865  iccpartlt  41866  icceuelpartlem  41877  iccpartnel  41880  pfx00  41890  pfx0  41891  fmtnoprmfac1  41983  fmtnoprmfac2  41985  prmdvdsfmtnof1lem2  42003  prminf2  42006  lighneallem4  42033  evenprm2  42129  even3prm2  42134  stgoldbwt  42170  upwlkbprop  42225  elsprel  42231  sprssspr  42237  sprsymrelfvlem  42246  nzerooringczr  42578  pgrpgt2nabl  42653  suppmptcfin  42666  linc1  42720  lindslinindsimp2lem5  42757  setrec2lem1  42946
  Copyright terms: Public domain W3C validator