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 183
Description: Inference eliminating an antecedent. (Contributed by NM, 5-Apr-1994.) (Proof shortened by Wolf Lammen, 19-Nov-2023.)
Hypotheses
Ref Expression
pm2.61i.1 (𝜑𝜓)
pm2.61i.2 𝜑𝜓)
Assertion
Ref Expression
pm2.61i 𝜓

Proof of Theorem pm2.61i
StepHypRef Expression
1 pm2.61i.1 . . 3 (𝜑𝜓)
2 pm2.61i.2 . . 3 𝜑𝜓)
31, 2nsyl4 161 . 2 𝜓𝜓)
43pm2.18i 131 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  184  pm2.61nii  185  pm2.61iii  186  pm2.65i  195  pm5.21nii  380  pm5.18  383  biass  386  pm2.61ian  808  ecase3  1024  4cases  1032  pm4.42  1045  ifpid  1067  elimh  1072  elimhOLD  1073  3ecase  1465  norass  1524  ax6e  2394  ax12  2440  exdistrf  2464  equvini  2472  equviniOLD  2473  ax12vALT  2487  2ax6e  2489  2ax6eOLD  2490  sb1  2499  sb2  2500  sb1OLD  2503  sb4a  2505  dfsb1  2506  dfsb2  2528  sbequiOLD  2530  sbi1OLD  2538  sbcom3  2544  sbco2  2549  sbco3  2551  sb9  2557  nfsbOLD  2562  sbalOLD  2571  dfsb2ALT  2587  sbequiALT  2592  sbi1ALT  2602  sbco2ALT  2611  eujustALT  2653  pm2.61ine  3100  ralcom2w  3363  ralcom2  3364  eueq2  3700  moeq3  3702  mo2icl  3704  sbc2or  3780  unineq  4253  csb0  4358  sbcel12  4359  sbcne12  4363  sbcel2  4366  csbidm  4381  csbun  4389  csbin  4390  ralidm  4453  ifsb  4478  ifid  4504  ifnot  4515  ifan  4516  ifor  4517  csbif  4520  elimhyp  4528  elimhyp2v  4529  elimhyp3v  4530  elimhyp4v  4531  elimdhyp  4533  keephyp2v  4535  keephyp3v  4536  rmosn  4649  rabsnif  4653  tppreqb  4732  ssunsn2  4754  n0snor2el  4758  preq12nebg  4787  opthprneg  4789  elpreqprlem  4790  dfopif  4794  csbuni  4860  disjord  5046  sbcbr  5113  unisn2  5208  intabs  5237  class2set  5246  dtru  5263  snexALT  5275  dtruALT  5280  axprlem3  5317  snex  5323  dtruALT2  5327  copsexgw  5373  copsexg  5374  snopeqop  5388  csbopab  5434  0nelopab  5444  dfid3  5456  csbxp  5644  csbres  5850  csbima12  5941  soirri  5980  csbrn  6054  dmsnopss  6065  dmsnsnsn  6071  opswap  6080  unixpid  6129  nsuceq0  6265  ordsssuc2  6273  iotassuni  6328  iotaex  6329  csbiota  6342  dffv3  6660  fvrn0  6692  ndmfv  6694  elfv2ex  6705  fveqres  6706  csbfv12  6707  csbfv  6709  dffv2  6750  fvco4i  6756  fvmptss  6773  fvmptex  6775  fvmptss2  6786  fvmptrabfv  6792  f0cli  6857  fvunsn  6934  fconst5  6961  csbriota  7118  riotassuni  7143  oprabidw  7176  csbov123  7187  csbov  7188  fvmptopab  7198  brfvopab  7200  elimdelov  7239  ovif12  7242  ndmovcl  7322  ndmovord  7327  elovmpt3imp  7391  difsnexi  7471  ordsuc  7517  ordsucelsuc  7525  1stval  7682  2ndval  7683  1st2val  7708  2nd2val  7709  el2mpocsbcl  7771  bropopvvv  7776  bropfvvvvlem  7777  bropfvvvv  7778  suppimacnv  7832  suppssdm  7834  ressuppss  7840  suppun  7841  extmptsuppeq  7845  funsssuppss  7847  fczsupp0  7850  suppss  7851  suppssov1  7853  suppss2  7855  suppssfv  7857  suppco  7861  supp0cosupp0OLD  7864  imacosuppOLD  7866  mpoxopynvov0  7875  mpoxopoveqd  7878  pwuninel  7932  smofvon2  7984  om0x  8135  brdomg  8508  snfi  8583  sdomirr  8643  domunsn  8656  2pwuninel  8661  snnen2o  8696  suppeqfsuppbi  8836  fsuppun  8841  funsnfsupp  8846  fipwuni  8879  oicl  8982  oif  8983  wemapso2  9006  card2on  9007  en2lp  9058  tctr  9171  r1tr  9194  rankdmr1  9219  r1pw  9263  r1pwALT  9264  rankuni  9281  scottex  9303  cardidm  9377  alephcard  9485  alephnbtwn  9486  cfub  9660  cardcf  9663  cflecard  9664  cfle  9665  cflim2  9674  cfidm  9686  isf32lem9  9772  itunisuc  9830  itunitc1  9831  itunitc  9832  ituniiun  9833  axcc2lem  9847  alephreg  9993  pwcfsdom  9994  cfpwsdom  9995  axunndlem1  10006  axpownd  10012  tskmcl  10252  addcompi  10305  addasspi  10306  mulcompi  10307  mulasspi  10308  distrpi  10309  addnidpi  10312  nlt1pi  10317  addcompq  10361  addcomnq  10362  mulcompq  10363  mulcomnq  10364  adderpq  10367  mulerpq  10368  addassnq  10369  mulassnq  10370  distrnq  10372  genpass  10420  addcompr  10432  mulcompr  10434  distrpr  10439  ltexprlem7  10453  addcomsr  10498  addasssr  10499  mulcomsr  10500  mulasssr  10501  distrsr  10502  uzssz  12253  uzwo  12300  nn01to3  12330  xnn0xaddcl  12618  elixx3g  12741  iooid  12756  elfz2  12889  injresinjlem  13147  injresinj  13148  fleqceilz  13212  modifeq2int  13291  modfzo0difsn  13301  addmodlteq  13304  ltweuz  13319  fzofi  13332  fsuppmapnn0fiubex  13350  hashrabrsn  13723  hashrabsn01  13724  hashrabsn1  13725  elprchashprn2  13747  hashss  13760  hashsn01  13767  hash1snb  13770  hashgt12el  13773  hashgt12el2  13774  hashgt23el  13775  hashfzp1  13782  hash2pwpr  13824  hashge2el2dif  13828  ffz0iswrd  13881  ccatsymb  13926  swrd00  13996  swrd0  14010  swrdwrdsymb  14014  pfx00  14026  pfx0  14027  repswswrd  14136  0csh0  14145  cshwcl  14150  cshwidxmod  14155  repswcshw  14164  cshw1  14174  s3sndisj  14317  s3iunsndisj  14318  xptrrel  14330  trclfvcotrg  14366  relexpfld  14398  reusq0  14812  modfsummods  15138  pwm1geoserOLD  15215  dvdsaddre2b  15647  gcdaddmlem  15862  prm23ge5  16142  pcmptcl  16217  prmgaplem5  16381  prmgaplem6  16382  cshwshash  16428  strfvss  16496  strfvi  16527  setsnid  16529  ressbas  16544  ressbasss  16546  resslem  16547  ress0  16548  ressress  16552  strle1  16582  0rest  16693  firest  16696  topnval  16698  xpsaddlem  16836  xpsvsca  16840  homffval  16950  comfffval  16958  oppchomfval  16974  oppcbas  16978  fullfunc  17166  fthfunc  17167  natfval  17206  fucbas  17220  fuchom  17221  arwval  17293  coafval  17314  xpcbas  17418  xpchomfval  17419  xpccofval  17422  lubfun  17580  glbfun  17593  oduval  17730  oduleval  17731  odumeet  17740  odujoin  17742  ipopos  17760  plusffval  17848  grpidval  17861  gsum0  17884  frmdplusg  18009  frmd0  18015  mgm2nsgrplem2  18024  mgm2nsgrplem3  18025  sgrp2rid2  18031  dfgrp2e  18069  grpinvfval  18082  grpinvfvalALT  18083  grpinvfvi  18086  grpsubfval  18087  grpsubfvalALT  18088  mulgfval  18166  mulgfvalALT  18167  mulgfvi  18170  cntrval  18389  oppgval  18415  oppgplusfval  18416  symgbas  18438  symgplusg  18447  psgnfval  18559  odfval  18591  odfvalALT  18592  oppglsm  18698  efgval  18774  mgpval  19173  mgpplusg  19174  ringidval  19184  opprval  19305  opprmulfval  19306  dvdsrval  19326  invrfval  19354  dvrfval  19365  staffval  19549  scaffval  19583  rlmval  19894  rlmsca2  19904  2idlval  19936  rrgval  19990  asclfval  20038  psrplusg  20091  psrmulr  20094  psrvscafval  20100  mplval  20138  mplcoe3  20177  evlval  20238  psr1val  20284  vr1val  20290  ply1val  20292  ply1basfvi  20339  ply1plusgfvi  20340  psr1sca2  20349  ply1sca2  20352  ply1ascl  20356  cply1mul  20392  gsummoncoe1  20402  evl1fval  20421  evl1fval1  20424  zrhval  20585  zlmlem  20594  zlmvsca  20599  chrval  20602  evpmss  20660  psgndiflemB  20674  ipffval  20722  thlbas  20770  thlle  20771  thloc  20773  pjfval  20780  dsmmval2  20810  mamufacex  20930  mavmulsolcl  21090  marrepfval  21099  marepvfval  21104  submafval  21118  mdetfval  21125  mdetfval1  21129  mdetunilem7  21157  mdetunilem8  21158  madufval  21176  minmar1fval  21185  mp2pm2mplem4  21347  toponsspwpw  21460  tgdif0  21530  indislem  21538  resstopn  21724  iocpnfordt  21753  icomnfordt  21754  hmeofval  22296  ussval  22797  nmfval  23127  nghmfval  23260  pcofval  23543  tcphval  23750  ioombl  24095  ibladdlem  24349  itgaddlem1  24352  iblabs  24358  dvbsss  24429  perfdvf  24430  mdegfval  24585  deg1fval  24603  deg1fvi  24608  uc1pval  24662  mon1pval  24664  2irrexpq  25240  lgsqrmodndvds  25857  gausslemma2dlem1a  25869  2lgs  25911  2sqreultblem  25952  2sqreunnltblem  25955  ttglem  26590  axcontlem12  26689  vtxval  26713  iedgval  26714  edgval  26762  usgr1v  26966  nbuhgr  27053  nbumgr  27057  uhgrnbgr0nb  27064  nbgr1vtx  27068  nbgrnself2  27070  nbusgrvtxm1  27089  sizusglecusg  27173  g0wlk0  27361  wlkreslem  27379  lfgrwlkprop  27397  wwlks  27541  wwlksn  27543  wspthsn  27554  iswwlksnon  27559  iswspthsnon  27562  0enwwlksnge1  27570  wwlksnfi  27612  wwlksnfiOLD  27613  clwwlk  27689  umgrclwwlkge2  27697  clwlkclwwlklem2a4  27703  clwwlkn  27732  clwwlknfiOLD  27752  clwwlknonmpo  27796  clwwlknon  27797  clwwlk0on0  27799  clwwlknon1le1  27808  1conngr  27901  eupth2lem3lem7  27941  frgr1v  27978  nfrgr2v  27979  1to2vfriswmgr  27986  2wspmdisj  28044  frgrreggt1  28100  frgrreg  28101  frgrregord013  28102  frgrogt3nreg  28104  friendship  28106  avril1  28170  vafval  28308  bafval  28309  smfval  28310  vsfval  28338  bcsiALT  28884  resvsca  30831  resvlem  30832  cntnevol  31387  signsw0glem  31723  bnj1189  32179  hashfundm  32252  fmlafvel  32530  gonan0  32537  satffun  32554  mvtval  32645  mexval  32647  mexval2  32648  mdvval  32649  mrsubfval  32653  mrsubrn  32658  msubfval  32669  elmsubrn  32673  msubrn  32674  mvhfval  32678  mpstval  32680  msrfval  32682  mstaval  32689  mppsval  32717  mthmval  32720  dfrdg3  32939  trpredlem1  32964  fvsingle  33279  unisnif  33284  funpartfv  33304  fullfunfv  33306  linedegen  33502  bj-ax6e  33899  axc11n11r  33915  bj-ax12v3ALT  33918  bj-dtru  34037  bj-sbsb  34058  bj-nfcsym  34113  bj-restsnid  34273  bj-inftyexpitaudisj  34380  bj-inftyexpidisj  34385  csbdif  34489  finxpreclem4  34558  finxp00  34566  isinf2  34569  wl-nfs1t  34659  matunitlindflem1  34770  itg2addnclem  34825  ibladdnclem  34830  itgaddnclem1  34832  iblabsnc  34838  iblmulc2nc  34839  ftc1anclem8  34856  ismgmOLD  35011  tsbi1  35294  tsbi2  35295  ac6s6  35333  equid1  35917  ax12fromc15  35923  equid1ALT  35943  dvelimf-o  35947  ax12inda2ALT  35964  ax12inda2  35965  sn-axprlem3  38989  sn-dtru  38991  mzpmfp  39224  itgocn  39644  mendbas  39664  mendplusgfval  39665  mendmulrfval  39667  mendsca  39669  mendvscafval  39670  arearect  39702  areaquad  39703  sn1dom  39772  or3or  40251  uneqsn  40253  addcomgi  40668  ax6e2ndeq  40773  2sb5ndVD  41124  2sb5ndALT  41146  sqwvfoura  42394  sqwvfourb  42395  fourierswlem  42396  fouriersw  42397  hspdifhsp  42779  hspmbllem2  42790  hspmbl  42792  tz6.12-afv  43253  ndmaovcl  43283  tz6.12-afv2  43320  otiunsndisjX  43359  fvmptrab  43372  nltle2tri  43394  fzopredsuc  43404  iccpartiltu  43429  iccpartigtl  43430  iccpartlt  43431  icceuelpartlem  43442  iccpartnel  43445  elsprel  43484  sprssspr  43490  sprsymrelfvlem  43499  prprelprb  43526  prprspr2  43527  fmtnoprmfac1  43574  fmtnoprmfac2  43576  prmdvdsfmtnof1lem2  43594  prminf2  43597  lighneallem4  43622  requad1  43634  requad2  43635  evenprm2  43726  even3prm2  43731  fpprbasnn  43741  stgoldbwt  43788  upwlkbprop  43860  efmndbas  43940  efmndplusg  43948  nzerooringczr  44241  pgrpgt2nabl  44312  suppmptcfin  44325  linc1  44378  lindslinindsimp2lem5  44415  reorelicc  44595  rrxsphere  44633  setrec2lem1  44694
  Copyright terms: Public domain W3C validator