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 174
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 171 . 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  175  pm2.61nii  176  pm2.61iii  177  pm2.65i  183  pm5.21nii  366  pm5.18  369  biass  372  pm2.61ian  826  ecase3  978  4cases  986  pm4.42  994  ifpid  1018  elimh  1023  elimhOLD  1026  3ecase  1428  ax6e  2237  ax12  2291  exdistrf  2320  ax12OLD  2328  equvini  2333  dfsb2  2360  sbequi  2362  sbi1  2379  sbcom3  2398  sbco2  2402  sbco3  2404  sb9  2413  ax12vALT  2415  hbs1  2423  nfsb  2427  2ax6e  2437  sbal  2449  eujustALT  2460  pm2.61ine  2864  ralcom2  3082  eueq2  3346  moeq3  3349  mo2icl  3351  sbc2or  3410  sbcimdvOLD  3465  unineq  3835  csb0  3933  sbcel12  3934  sbcne12  3937  sbcel2  3940  csbidm  3953  csbun  3960  csbin  3961  ralidm  4026  ifsb  4048  ifid  4074  ifnot  4082  ifan  4083  ifor  4084  csbif  4087  elimhyp  4095  elimhyp2v  4096  elimhyp3v  4097  elimhyp4v  4098  elimdhyp  4100  keephyp2v  4102  keephyp3v  4103  eqoreldifOLD  4172  rabsnif  4201  tppreqb  4276  ssunsn2  4296  elpreqprlem  4328  dfopif  4331  csbuni  4396  sbcbr  4631  unisn2  4717  intabs  4747  class2set  4753  snexALT  4773  dtru  4778  dtruALT  4821  snex  4830  dtruALT2  4833  copsexg  4876  csbopab  4922  dfid3  4944  csbxp  5113  csbres  5307  csbima12  5389  soirri  5428  csbrn  5500  dmsnopss  5511  dmsnsnsn  5517  opswap  5526  unixpid  5573  nsuceq0  5708  ordsssuc2  5717  iotassuni  5770  iotaex  5771  dfiota4  5782  csbiota  5783  dffv3  6084  fvrn0  6111  ndmfv  6113  elfv2ex  6124  fveqres  6125  csbfv12  6126  csbfv  6128  dffv2  6166  fvco4i  6171  fvmptss  6186  fvmptex  6188  fvmptss2  6197  f0cli  6263  fvunsn  6328  fconst5  6354  csbriota  6501  riotassuni  6525  csbov123  6563  csbov  6564  0neqopab  6574  brfvopab  6576  elimdelov  6612  ovif12  6615  ndmovcl  6694  ndmovord  6699  elovmpt3imp  6765  difsnexi  6841  ordsuc  6883  ordsucelsuc  6891  1stval  7038  2ndval  7039  1st2val  7062  2nd2val  7063  el2mpt2csbcl  7114  bropopvvv  7119  bropfvvvvlem  7120  bropfvvvv  7121  suppimacnv  7170  suppssdm  7172  ressuppss  7178  suppun  7179  extmptsuppeq  7183  funsssuppss  7185  fczsupp0  7188  suppss  7189  suppssov1  7191  suppss2  7193  suppssfv  7195  supp0cosupp0  7198  imacosupp  7199  mpt2xopynvov0  7208  mpt2xopoveqd  7211  pwuninel  7265  smofvon2  7317  om0x  7463  brdomg  7828  snfi  7900  sdomirr  7959  domunsn  7972  2pwuninel  7977  snnen2o  8011  suppeqfsuppbi  8149  fsuppun  8154  funsnfsupp  8159  fipwuni  8192  oicl  8294  oif  8295  wemapso2  8318  card2on  8319  en2lp  8370  tctr  8476  r1tr  8499  rankdmr1  8524  r1pw  8568  r1pwALT  8569  rankuni  8586  scottex  8608  cardidm  8645  alephcard  8753  alephnbtwn  8754  cdacomen  8863  cfub  8931  cardcf  8934  cflecard  8935  cfle  8936  cflim2  8945  cfidm  8957  isf32lem9  9043  itunisuc  9101  itunitc1  9102  itunitc  9103  ituniiun  9104  axcc2lem  9118  alephreg  9260  pwcfsdom  9261  cfpwsdom  9262  axunndlem1  9273  axpownd  9279  tskmcl  9519  addcompi  9572  addasspi  9573  mulcompi  9574  mulasspi  9575  distrpi  9576  addnidpi  9579  nlt1pi  9584  addcompq  9628  addcomnq  9629  mulcompq  9630  mulcomnq  9631  adderpq  9634  mulerpq  9635  addassnq  9636  mulassnq  9637  distrnq  9639  genpass  9687  addcompr  9699  mulcompr  9701  distrpr  9706  ltexprlem7  9720  addcomsr  9764  addasssr  9765  mulcomsr  9766  mulasssr  9767  distrsr  9768  uzssz  11539  uzwo  11583  nn01to3  11613  elixx3g  12015  iooid  12030  elfz2  12159  injresinjlem  12405  injresinj  12406  fleqceilz  12470  modifeq2int  12549  modfzo0difsn  12559  addmodlteq  12562  ltweuz  12577  fzofi  12590  fsuppmapnn0fiubex  12609  hashrabrsn  12974  hashrabsn01  12975  hashrabsn1  12976  elprchashprn2  12997  hashss  13010  hashsn01  13017  hash1snb  13020  hashgt12el  13022  hashgt12el2  13023  hashfzp1  13030  hash2pwpr  13065  hashge2el2dif  13067  ccatsymb  13165  swrd00  13216  swrd0  13232  swrdccatin1  13280  repswswrd  13328  0csh0  13336  cshwcl  13341  cshwidxmod  13346  repswcshw  13355  cshw1  13365  s3sndisj  13500  s3iunsndisj  13501  xptrrel  13513  trclfvcotrg  13551  relexpfld  13583  modfsummods  14312  pwm1geoser  14385  dvdsaddre2b  14813  zeneo  14847  gcdaddmlem  15029  prm23ge5  15304  pcmptcl  15379  prmgaplem5  15543  prmgaplem6  15544  cshwshash  15595  strfvss  15659  strfvi  15687  setsnid  15689  ressbas  15703  ressbasss  15705  resslem  15706  ress0  15707  ressress  15711  strle1  15746  0rest  15859  firest  15862  topnval  15864  xpsaddlem  16004  xpsvsca  16008  homffval  16119  comfffval  16127  oppchomfval  16143  oppcbas  16147  fullfunc  16335  fthfunc  16336  natfval  16375  fucbas  16389  fuchom  16390  arwval  16462  coafval  16483  xpcbas  16587  xpchomfval  16588  xpccofval  16591  lubfun  16749  glbfun  16762  oduval  16899  oduleval  16900  odumeet  16909  odujoin  16911  ipopos  16929  plusffval  17016  grpidval  17029  gsum0  17047  frmdplusg  17160  frmd0  17166  mgm2nsgrplem2  17175  mgm2nsgrplem3  17176  sgrp2rid2  17182  dfgrp2e  17217  grpinvfval  17229  grpinvfvi  17232  grpsubfval  17233  mulgfval  17311  mulgfvi  17314  cntrval  17521  oppgval  17546  oppgplusfval  17547  symgbas  17569  symgplusg  17578  psgnfval  17689  odfval  17721  oppglsm  17826  efgval  17899  mgpval  18261  mgpplusg  18262  ringidval  18272  opprval  18393  opprmulfval  18394  dvdsrval  18414  invrfval  18442  dvrfval  18453  staffval  18616  scaffval  18650  rlmval  18958  rlmsca2  18968  2idlval  19000  rrgval  19054  asclfval  19101  psrplusg  19148  psrmulr  19151  psrvscafval  19157  mplval  19195  mplcoe3  19233  evlval  19291  psr1val  19323  vr1val  19329  ply1val  19331  ply1basfvi  19378  ply1plusgfvi  19379  psr1sca2  19388  ply1sca2  19391  ply1ascl  19395  cply1mul  19431  gsummoncoe1  19441  evl1fval  19459  evl1fval1  19462  zrhval  19620  zlmlem  19629  zlmvsca  19634  chrval  19637  evpmss  19696  psgndiflemB  19710  ipffval  19757  thlbas  19801  thlle  19802  thloc  19804  pjfval  19811  dsmmval2  19841  mamufacex  19956  mavmulsolcl  20118  marrepfval  20127  marepvfval  20132  submafval  20146  mdetfval  20153  mdetfval1  20157  mdetunilem7  20185  mdetunilem8  20186  madufval  20204  minmar1fval  20213  mp2pm2mplem4  20375  tgdif0  20549  indislem  20556  resstopn  20742  iocpnfordt  20771  icomnfordt  20772  hmeofval  21313  ussval  21815  nmfval  22144  nghmfval  22268  pcofval  22549  tchval  22746  ioombl  23057  ibladdlem  23309  itgaddlem1  23312  iblabs  23318  dvbsss  23389  perfdvf  23390  mdegfval  23543  deg1fval  23561  deg1fvi  23566  uc1pval  23620  mon1pval  23622  lgsqrmodndvds  24795  gausslemma2dlem1a  24807  2lgs  24849  ttglem  25474  axcontlem12  25573  usgraedgprv  25671  usgra1v  25685  nbusgra  25723  nbgra0nb  25724  nbgranself2  25731  cusgra1v  25756  uvtxisvtx  25784  uvtx0  25785  uvtx01vtx  25786  1conngra  25969  wwlknfi  26032  wlk0  26055  clwwlkprop  26064  clwwlkgt0  26065  clwwlknprop  26066  clwlkisclwwlklem2a4  26078  2wlkonot3v  26168  2spthonot3v  26169  vdgrf  26191  nbhashuvtx1  26208  frgra2v  26292  1to2vfriswmgra  26299  2pthfrgra  26304  frgrancvvdeqlem2  26324  2spotdisj  26354  2spotiundisj  26355  2spotmdisj  26361  frgrareggt1  26409  frgrareg  26410  frgraregord013  26411  frgraogt3nreg  26413  friendship  26415  avril1  26477  vafval  26626  bafval  26627  smfval  26628  vsfval  26658  bcsiALT  27226  resvsca  28967  resvlem  28968  cntnevol  29424  signsw0glem  29762  bnj1189  30137  mvtval  30457  mexval  30459  mexval2  30460  mdvval  30461  mrsubfval  30465  mrsubrn  30470  msubfval  30481  elmsubrn  30485  msubrn  30486  mvhfval  30490  mpstval  30492  msrfval  30494  mstaval  30501  mppsval  30529  mthmval  30532  dfrdg3  30752  trpredlem1  30777  bdayelon  30885  fvsingle  31003  unisnif  31008  funpartfv  31028  fullfunfv  31030  linedegen  31226  bj-ax6e  31648  axc11n11r  31666  bj-ax12v3ALT  31669  bj-dtru  31791  bj-sbsb  31818  bj-nfcsym  31875  bj-restsnid  32017  bj-toponss  32037  bj-inftyexpidisj  32070  csbdif  32143  finxpreclem4  32203  finxp00  32211  wl-nfs1t  32299  wl-sbcom3  32347  matunitlindflem1  32371  itg2addnclem  32427  ibladdnclem  32432  itgaddnclem1  32434  iblabsnc  32440  iblmulc2nc  32441  ftc1anclem8  32458  ismgmOLD  32615  tsbi1  32906  tsbi2  32907  ac6s6  32946  equid1  32998  ax12fromc15  33004  equid1ALT  33024  dvelimf-o  33028  ax12inda2ALT  33045  ax12inda2  33046  mzpmfp  36124  itgocn  36549  mendbas  36569  mendplusgfval  36570  mendmulrfval  36572  mendsca  36574  mendvscafval  36575  arearect  36616  areaquad  36617  or3or  37135  uneqsn  37137  addcomgi  37477  ax6e2ndeq  37592  2sb5ndVD  37964  2sb5ndALT  37986  sqwvfoura  38918  sqwvfourb  38919  fourierswlem  38920  fouriersw  38921  hspdifhsp  39303  hspmbllem2  39314  hspmbl  39316  tz6.12-afv  39700  ndmaovcl  39730  nltle2tri  39740  fzopredsuc  39744  iccpartiltu  39758  iccpartigtl  39759  iccpartlt  39760  icceuelpartlem  39771  iccpartnel  39774  fmtnoprmfac1  39813  fmtnoprmfac2  39815  prmdvdsfmtnof1lem2  39833  prminf2  39836  lighneallem4  39863  evenprm2  39959  stgoldbwt  39996  pfx00  40045  pfx0  40046  n0snor2el  40116  otiunsndisjX  40125  xnn0xaddcl  40208  usgr1v  40477  nbuhgr  40560  nbumgr  40564  uhgrnbgr0nb  40571  nbgr1vtx  40575  nbgrnself2  40580  nbusgrvtxm1  40602  uvtxa0  40615  sizusglecusg  40674  wlkbProp  40812  g01wlk0  40855  1wlkreslem  40873  lfgrwlkprop  40891  wwlks  41033  wwlksn  41035  wspthsn  41041  iswwlksnon  41046  iswspthsnon  41047  0enwwlksnge1  41055  wwlksnfi  41107  wwlksnonfi  41122  wspn0  41126  wwlks2onv  41153  2wspdisj  41160  2wspiundisj  41161  clwwlks  41182  clwwlksn  41184  clwlkclwwlklem2a4  41201  umgrclwwlksge2  41214  clwwlksnfi  41215  1conngr  41356  eupth2lem3lem7  41397  frgr1v  41436  nfrgr2v  41437  1to2vfriswmgr  41444  frgrncvvdeqlem2  41465  2wspmdisj  41496  av-frgrareggt1  41542  av-frgrareg  41543  av-frgraregord013  41544  av-frgraogt3nreg  41546  av-friendship  41548  nzerooringczr  41859  pgrpgt2nabl  41936  suppmptcfin  41949  linc1  42003  lindslinindsimp2lem5  42040
  Copyright terms: Public domain W3C validator