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 174 . 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  369  pm5.18  372  biass  375  pm2.61ian  837  ecase3  1046  4cases  1054  pm4.42  1069  ifpid  1091  elimh  1096  3ecase  1591  ax6e  2426  ax12  2474  exdistrf  2497  equvini  2506  dfsb2  2534  sbequi  2536  sbi1  2553  sbcom3  2572  sbco2  2576  sbco3  2578  sb9  2587  ax12vALT  2589  hbs1OLD  2591  nfsb  2605  2ax6e  2613  sbal  2625  eujustALT  2644  pm2.61ine  3072  ralcom2  3303  eueq2  3589  moeq3  3592  mo2icl  3594  sbc2or  3653  unineq  4090  csb0  4190  sbcel12  4191  sbcne12  4194  sbcel2  4197  csbidm  4210  csbun  4218  csbin  4219  ralidm  4281  ifsb  4303  ifid  4329  ifnot  4340  ifan  4341  ifor  4342  csbif  4345  elimhyp  4353  elimhyp2v  4354  elimhyp3v  4355  elimhyp4v  4356  elimdhyp  4358  keephyp2v  4360  keephyp3v  4361  rabsnif  4460  tppreqb  4537  ssunsn2  4559  n0snor2el  4563  preq12nebg  4596  opthprneg  4598  elpreqprlem  4599  dfopif  4603  csbuni  4671  disjord  4844  sbcbr  4910  unisn2  5002  intabs  5030  class2set  5037  dtru  5053  snexALT  5065  dtruALT  5070  snex  5111  dtruALT2  5114  copsexg  5158  snopeqop  5173  csbopab  5216  dfid3  5233  csbxp  5415  csbres  5613  csbima12  5706  soirri  5746  csbrn  5820  dmsnopss  5832  dmsnsnsn  5838  opswap  5849  unixpid  5897  nsuceq0  6030  ordsssuc2  6038  iotassuni  6089  iotaex  6090  dfiota4OLD  6102  csbiota  6103  dffv3  6413  fvrn0  6445  ndmfv  6447  elfv2ex  6458  fveqres  6459  csbfv12  6460  csbfv  6462  dffv2  6501  fvco4i  6506  fvmptss  6522  fvmptex  6524  fvmptss2  6534  fvmptrabfv  6539  f0cli  6601  fvunsn  6679  fconst5  6705  csbriota  6856  riotassuni  6881  csbov123  6924  csbov  6925  fvmptopab  6936  0neqopab  6937  brfvopab  6939  elimdelov  6975  ovif12  6978  ndmovcl  7058  ndmovord  7063  elovmpt3imp  7129  difsnexi  7209  ordsuc  7253  ordsucelsuc  7261  1stval  7409  2ndval  7410  1st2val  7435  2nd2val  7436  el2mpt2csbcl  7492  bropopvvv  7498  bropfvvvvlem  7499  bropfvvvv  7500  suppimacnv  7549  suppssdm  7551  ressuppss  7557  suppun  7558  extmptsuppeq  7562  funsssuppss  7565  fczsupp0  7568  suppss  7569  suppssov1  7571  suppss2  7573  suppssfv  7575  supp0cosupp0  7578  imacosupp  7579  mpt2xopynvov0  7588  mpt2xopoveqd  7591  pwuninel  7645  smofvon2  7698  om0x  7845  brdomg  8211  snfi  8286  sdomirr  8345  domunsn  8358  2pwuninel  8363  snnen2o  8397  suppeqfsuppbi  8537  fsuppun  8542  funsnfsupp  8547  fipwuni  8580  oicl  8682  oif  8683  wemapso2  8706  card2on  8707  en2lp  8758  tctr  8872  r1tr  8895  rankdmr1  8920  r1pw  8964  r1pwALT  8965  rankuni  8982  scottex  9004  cardidm  9077  alephcard  9185  alephnbtwn  9186  cdacomen  9297  cfub  9365  cardcf  9368  cflecard  9369  cfle  9370  cflim2  9379  cfidm  9391  isf32lem9  9477  itunisuc  9535  itunitc1  9536  itunitc  9537  ituniiun  9538  axcc2lem  9552  alephreg  9698  pwcfsdom  9699  cfpwsdom  9700  axunndlem1  9711  axpownd  9717  tskmcl  9957  addcompi  10010  addasspi  10011  mulcompi  10012  mulasspi  10013  distrpi  10014  addnidpi  10017  nlt1pi  10022  addcompq  10066  addcomnq  10067  mulcompq  10068  mulcomnq  10069  adderpq  10072  mulerpq  10073  addassnq  10074  mulassnq  10075  distrnq  10077  genpass  10125  addcompr  10137  mulcompr  10139  distrpr  10144  ltexprlem7  10158  addcomsr  10202  addasssr  10203  mulcomsr  10204  mulasssr  10205  distrsr  10206  uzssz  11943  uzwo  11989  nn01to3  12019  xnn0xaddcl  12303  elixx3g  12425  iooid  12440  elfz2  12575  injresinjlem  12831  injresinj  12832  fleqceilz  12896  modifeq2int  12975  modfzo0difsn  12985  addmodlteq  12988  ltweuz  13003  fzofi  13016  fsuppmapnn0fiubex  13034  hashrabrsn  13398  hashrabsn01  13399  hashrabsn1  13400  elprchashprn2  13420  hashss  13433  hashsn01  13440  hash1snb  13443  hashgt12el  13446  hashgt12el2  13447  hashfzp1  13454  hash2pwpr  13494  hashge2el2dif  13498  ccatsymb  13598  swrd00  13660  swrd0  13677  swrdccatin1  13726  repswswrd  13774  0csh0  13782  cshwcl  13787  cshwidxmod  13792  repswcshw  13801  cshw1  13811  s3sndisj  13950  s3iunsndisj  13951  xptrrel  13963  trclfvcotrg  13999  relexpfld  14031  modfsummods  14766  pwm1geoser  14841  dvdsaddre2b  15271  gcdaddmlem  15483  prm23ge5  15756  pcmptcl  15831  prmgaplem5  15995  prmgaplem6  15996  cshwshash  16042  strfvss  16110  strfvi  16143  setsnid  16145  ressbas  16160  ressbasss  16162  resslem  16163  ress0  16164  ressress  16169  strle1  16203  0rest  16314  firest  16317  topnval  16319  xpsaddlem  16459  xpsvsca  16463  homffval  16573  comfffval  16581  oppchomfval  16597  oppcbas  16601  fullfunc  16789  fthfunc  16790  natfval  16829  fucbas  16843  fuchom  16844  arwval  16916  coafval  16937  xpcbas  17042  xpchomfval  17043  xpccofval  17046  lubfun  17204  glbfun  17217  oduval  17354  oduleval  17355  odumeet  17364  odujoin  17366  ipopos  17384  plusffval  17471  grpidval  17484  gsum0  17502  frmdplusg  17615  frmd0  17621  mgm2nsgrplem2  17630  mgm2nsgrplem3  17631  sgrp2rid2  17637  dfgrp2e  17672  grpinvfval  17684  grpinvfvi  17687  grpsubfval  17688  mulgfval  17766  mulgfvi  17769  cntrval  17972  oppgval  17997  oppgplusfval  17998  symgbas  18020  symgplusg  18029  psgnfval  18140  odfval  18172  oppglsm  18277  efgval  18350  mgpval  18713  mgpplusg  18714  ringidval  18724  opprval  18845  opprmulfval  18846  dvdsrval  18866  invrfval  18894  dvrfval  18905  staffval  19070  scaffval  19104  rlmval  19419  rlmsca2  19429  2idlval  19461  rrgval  19515  asclfval  19562  psrplusg  19609  psrmulr  19612  psrvscafval  19618  mplval  19656  mplcoe3  19694  evlval  19751  psr1val  19783  vr1val  19789  ply1val  19791  ply1basfvi  19838  ply1plusgfvi  19839  psr1sca2  19848  ply1sca2  19851  ply1ascl  19855  cply1mul  19891  gsummoncoe1  19901  evl1fval  19919  evl1fval1  19922  zrhval  20083  zlmlem  20092  zlmvsca  20097  chrval  20100  evpmss  20158  psgndiflemB  20173  ipffval  20222  thlbas  20270  thlle  20271  thloc  20273  pjfval  20280  dsmmval2  20310  mamufacex  20425  mavmulsolcl  20588  marrepfval  20597  marepvfval  20602  submafval  20616  mdetfval  20623  mdetfval1  20627  mdetunilem7  20655  mdetunilem8  20656  madufval  20674  minmar1fval  20683  mp2pm2mplem4  20847  toponsspwpw  20960  tgdif0  21030  indislem  21038  resstopn  21224  iocpnfordt  21253  icomnfordt  21254  hmeofval  21795  ussval  22296  nmfval  22626  nghmfval  22759  pcofval  23042  tchval  23249  ioombl  23568  ibladdlem  23822  itgaddlem1  23825  iblabs  23831  dvbsss  23902  perfdvf  23903  mdegfval  24058  deg1fval  24076  deg1fvi  24081  uc1pval  24135  mon1pval  24137  lgsqrmodndvds  25314  gausslemma2dlem1a  25326  2lgs  25368  ttglem  25992  axcontlem12  26091  vtxval  26114  iedgval  26115  edgval  26177  usgr1v  26386  nbuhgr  26477  nbumgr  26481  uhgrnbgr0nb  26488  nbgr1vtx  26492  nbgrnself2  26494  nbgrnself2OLD  26497  nbusgrvtxm1  26519  sizusglecusg  26609  g0wlk0  26798  wlkreslem  26816  lfgrwlkprop  26834  wwlks  26978  wwlksn  26980  wspthsn  26992  iswwlksnon  26997  iswwlksnonOLD  26998  iswspthsnon  27001  iswspthsnonOLD  27002  0enwwlksnge1  27013  wwlksnfi  27065  clwwlk  27148  umgrclwwlkge2  27156  clwlkclwwlklem2a4  27162  clwwlkn  27193  clwwlknOLD  27194  clwwlknfi  27216  clwwlknonmpt2  27276  clwwlknon  27277  clwwlk0on0  27281  clwwlknon1le1  27291  1conngr  27389  eupth2lem3lem7  27429  frgr1v  27468  nfrgr2v  27469  1to2vfriswmgr  27476  2wspmdisj  27534  frgrreggt1  27603  frgrreg  27604  frgrregord013  27605  frgrogt3nreg  27607  friendship  27609  avril1  27672  vafval  27808  bafval  27809  smfval  27810  vsfval  27838  bcsiALT  28386  resvsca  30177  resvlem  30178  cntnevol  30638  signsw0glem  30977  bnj1189  31421  mvtval  31741  mexval  31743  mexval2  31744  mdvval  31745  mrsubfval  31749  mrsubrn  31754  msubfval  31765  elmsubrn  31769  msubrn  31770  mvhfval  31774  mpstval  31776  msrfval  31778  mstaval  31785  mppsval  31813  mthmval  31816  dfrdg3  32043  trpredlem1  32068  fvsingle  32369  unisnif  32374  funpartfv  32394  fullfunfv  32396  linedegen  32592  bj-ax6e  32989  axc11n11r  33009  bj-ax12v3ALT  33012  bj-dtru  33129  bj-sbsb  33155  bj-nfcsym  33212  bj-restsnid  33369  bj-inftyexpidisj  33432  csbdif  33506  finxpreclem4  33565  finxp00  33573  wl-nfs1t  33656  matunitlindflem1  33736  itg2addnclem  33791  ibladdnclem  33796  itgaddnclem1  33798  iblabsnc  33804  iblmulc2nc  33805  ftc1anclem8  33822  ismgmOLD  33978  tsbi1  34268  tsbi2  34269  ac6s6  34308  equid1  34696  ax12fromc15  34702  equid1ALT  34722  dvelimf-o  34726  ax12inda2ALT  34743  ax12inda2  34744  mzpmfp  37829  itgocn  38252  mendbas  38272  mendplusgfval  38273  mendmulrfval  38275  mendsca  38277  mendvscafval  38278  arearect  38318  areaquad  38319  or3or  38836  uneqsn  38838  addcomgi  39175  ax6e2ndeq  39290  2sb5ndVD  39657  2sb5ndALT  39679  sqwvfoura  40941  sqwvfourb  40942  fourierswlem  40943  fouriersw  40944  hspdifhsp  41329  hspmbllem2  41340  hspmbl  41342  tz6.12-afv  41779  ndmaovcl  41809  tz6.12-afv2  41846  otiunsndisjX  41886  fvmptrab  41899  nltle2tri  41915  fzopredsuc  41925  iccpartiltu  41950  iccpartigtl  41951  iccpartlt  41952  icceuelpartlem  41963  iccpartnel  41966  pfx00  41976  pfx0  41977  fmtnoprmfac1  42069  fmtnoprmfac2  42071  prmdvdsfmtnof1lem2  42089  prminf2  42092  lighneallem4  42119  evenprm2  42215  even3prm2  42220  stgoldbwt  42256  upwlkbprop  42304  elsprel  42310  sprssspr  42316  sprsymrelfvlem  42325  nzerooringczr  42657  pgrpgt2nabl  42732  suppmptcfin  42745  linc1  42799  lindslinindsimp2lem5  42836  setrec2lem1  43025
  Copyright terms: Public domain W3C validator