MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  anbi2d Unicode version

Theorem anbi2d 703
Description: Deduction adding a left conjunct to both sides of a logical equivalence. (Contributed by NM, 11-May-1993.) (Proof shortened by Wolf Lammen, 16-Nov-2013.)
Hypothesis
Ref Expression
bid.1
Assertion
Ref Expression
anbi2d

Proof of Theorem anbi2d
StepHypRef Expression
1 bid.1 . . 3
21a1d 25 . 2
32pm5.32d 639 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369
This theorem is referenced by:  anbi2  707  anbi12d  710  bi2anan9  873  2eu6OLD  2384  eleq2dALT  2528  eleq2OLD  2532  ceqsex2  3147  ceqsex6v  3151  vtocl2gaf  3174  vtocl4ga  3179  ceqsrex2v  3235  moeq3  3276  mob2  3279  eqreu  3291  reu2eqd  3296  nelrdva  3309  undif4  3883  r19.27z  3928  r19.27zv  3929  ssunsn2  4189  preq12bg  4209  prel12g  4210  opeq2  4218  ralunsn  4237  intab  4317  disjxun  4450  opabbid  4514  opthg  4727  pocl  4812  isso2i  4837  ordelord  4905  ordtri4  4920  xpeq2  5019  rabxp  5041  vtoclr  5049  opeliunxp  5056  posn  5073  opbrop  5084  elrnmpt1  5256  dfres2  5331  brcodir  5391  poltletr  5407  xp11  5447  fununi  5659  fneq2  5675  fnun  5692  feq3  5720  foeq3  5798  funbrfv  5911  ssimaexg  5939  fvopab3g  5952  fvopab3ig  5953  fvelrn  6024  fvcofneq  6039  fmptco  6064  elunirn  6163  f12dfv  6179  f13dfv  6180  isoeq2  6216  isoeq3  6217  isoini  6234  isopolem  6241  f1oiso  6247  f1oiso2  6248  riotabidv  6259  oprabv  6345  oprabbid  6350  cbvoprab3  6373  mpt2mptx  6393  mpt2fun  6404  elrnmpt2res  6416  ov  6422  ov3  6439  ov6g  6440  ovg  6441  caoftrn  6575  dfwe2  6617  dflim4  6683  tfisi  6693  elxp4  6744  elxp5  6745  f1o2ndf1  6908  frxp  6910  xporderlem  6911  fnwelem  6915  brtpos2  6980  dftpos4  6993  onfununi  7031  recseq  7062  omopth  7326  brecop  7423  eroveu  7425  erovlem  7426  erov  7427  ecopovtrn  7433  elpmg  7454  ixpsnval  7492  ixpsnf1o  7529  domeng  7550  dom2lem  7575  xpcomco  7627  xpassen  7631  xpdom2  7632  omxpenlem  7638  xpf1o  7699  unxpdom  7747  isinf  7753  findcard2  7780  findcard2d  7782  fiint  7817  supeq2  7928  wemapso2lem  7999  inf0  8059  cantnfp1lem3  8120  cantnfp1  8121  scott0  8325  isinffi  8394  isacn  8446  aceq1  8519  aceq0  8520  aceq2  8521  dfac3  8523  dfac5lem1  8525  dfac2  8532  dfac12lem2  8545  kmlem8  8558  kmlem14  8564  infmap2  8619  cfval  8648  cflim3  8663  sornom  8678  infpssrlem4  8707  isf32lem9  8762  domtriomlem  8843  axdc2lem  8849  zfac  8861  ac6num  8880  axrepndlem1  8988  axunndlem1  8991  axregnd  9002  axregndOLD  9003  axinfndlem1  9004  axacndlem4  9009  axacndlem5  9010  zfcndac  9018  fpwwe2lem5  9033  pwfseqlem4a  9060  pwfseqlem4  9061  alephgch  9073  wunex2  9137  tskord  9179  nqereu  9328  ordpipq  9341  prcdnq  9392  prnmax  9394  genpnnp  9404  distrlem5pr  9426  ltprord  9429  ltexprlem3  9437  ltexprlem4  9438  ltexpri  9442  prlem936  9446  reclem2pr  9447  addsrmo  9471  mulsrmo  9472  addsrpr  9473  mulsrpr  9474  ltsosr  9492  mulgt0sr  9503  ltresr  9538  axpre-lttrn  9564  axpre-mulgt0  9566  eqlelt  9693  lesub0  10094  wloglei  10110  mulle0b  10438  sup3  10525  infm3  10527  prime  10968  fzind  10987  uzwo  11173  uzwoOLD  11174  zbtwnre  11209  xltnegi  11444  xmulneg1  11490  ixxval  11566  fzval  11703  elfzm11  11778  elfzo  11831  seqof2  12165  nn0opth2  12352  facwordi  12367  hashnn0n0nn  12458  brfi1uzind  12532  wrdeqswrdlsw  12674  2swrd1eqwrdeq  12679  wrd2ind  12703  cshwcsh2id  12796  2swrd2eqwrdeq  12891  shftfval  12903  shftfib  12905  shftfn  12906  2shfti  12913  abs1m  13168  cau3lem  13187  caubnd2  13190  clim  13317  rlim  13318  clim2  13327  climi  13333  o1lo1  13360  rlimcn2  13413  climcn2  13415  addcn2  13416  subcn2  13417  mulcn2  13418  o1of2  13435  isercoll  13490  caurcvg2  13500  sumeq2w  13514  sumeq2ii  13515  summo  13539  fsum  13542  prodfdiv  13705  ntrivcvgn0  13707  ntrivcvgmullem  13710  prodeq1f  13715  prodeq2w  13719  prodeq2ii  13720  prodmo  13743  zprod  13744  fprod  13748  fprodntriv  13749  sinbnd  13915  cosbnd  13916  divalgb  14062  ndvdssub  14065  smupp1  14130  smueqlem  14140  gcdval  14146  gcdcllem2  14150  gcdneg  14164  gcdass  14183  algcvgblem  14206  prmind2  14228  qredeq  14247  euclemma  14249  qnumval  14270  qdenval  14271  eulerthlem2  14312  pceu  14370  pczpre  14371  pcdiv  14376  prmpwdvds  14422  prmreclem5  14438  vdwapun  14492  ramub2  14532  rami  14533  ramcl  14547  ismred2  15000  isacs  15048  iscatd2  15078  catpropd  15104  oppccatid  15114  isinv  15154  isssc  15189  funcres2b  15266  funcpropd  15269  fucinv  15342  yoniso  15554  prslem  15560  drsdir  15564  drsdirfi  15567  posi  15579  isposd  15585  pltval  15590  plttr  15600  isipodrs  15791  ipodrsima  15795  dirge  15867  gsumpropd  15899  gsumress  15903  mnd1OLD  15962  mrcmndind  15997  mgmnsgrpex  16049  qusgrp2  16188  resscntz  16369  psgnunilem3  16521  psgneu  16531  psgnvali  16533  psgnvalii  16534  isslw  16628  subgslw  16636  iscmnd  16810  gsumval3eu  16907  gsumval3OLD  16908  gsumval3lem2  16910  telgsumfzs  17018  dmdprd  17029  subgdmdprd  17081  dprd2d2  17093  pgpfac1  17131  pgpfaclem2  17133  pgpfaclem3  17134  pgpfac  17135  ablfaclem1  17136  qusring2  17269  dvdsrval  17294  crngunit  17311  dfrhm2  17366  isdrngd  17421  abvpropd  17491  islmod  17516  lssacs  17613  lsspropd  17663  islmhm  17673  lbspropd  17745  ixpsnbasval  17855  fiidomfld  17957  ltbval  18136  opsrval  18139  mpfind  18205  coe1fzgsumd  18344  pf1ind  18391  evl1gsumd  18393  psgndiflemA  18637  pjfval2  18740  frlmup1  18832  scmatf1  19033  mdetralt  19110  mdetralt2  19111  mdetunilem1  19114  mdetunilem2  19115  mdetunilem9  19122  gsummatr01  19161  eltopspOLD  19419  istpsOLD  19421  basis2  19452  eltg2  19459  isclo  19588  isnei  19604  isneip  19606  neiptopnei  19633  restbas  19659  restcld  19673  neitr  19681  iscnp  19738  iscnp3  19745  tgcn  19753  cnpimaex  19757  lmbrf  19761  cncnp  19781  cnprest2  19791  isreg  19833  regsep  19835  isnrm  19836  ist1-2  19848  nrmsep3  19856  isnrm2  19859  hauscmplem  19906  dfcon2  19920  is1stc  19942  1stcclb  19945  1stcfb  19946  is2ndc  19947  2ndc1stc  19952  1stcrest  19954  2ndcsep  19960  1stccnp  19963  islly  19969  llyeq  19971  llyi  19975  hausllycmp  19995  lly1stc  19997  islocfin  20018  txbas  20068  ptpjpre1  20072  elpt  20073  txcnpi  20109  ptpjopn  20113  ptcldmpt  20115  ptclsg  20116  txcnp  20121  ptcnp  20123  hausdiag  20146  tx1stc  20151  xkoinjcn  20188  imasnopn  20191  imasncld  20192  imasncls  20193  fbfinnfr  20342  snfil  20365  uffix2  20425  elfm  20448  elfm2  20449  fmco  20462  hauspwpwf1  20488  flfnei  20492  isflf  20494  lmflf  20506  fclscf  20526  isfcf  20535  alexsublem  20544  cnextcn  20567  cnextfres  20568  eltsms  20631  tsmsresOLD  20645  tsmsres  20646  tsmsf1o  20647  ustuqtop4  20747  ispsmet  20808  ismet  20826  isxmet  20827  ismet2  20836  imasdsf1olem  20876  blres  20934  met2ndc  21026  metcnp3  21043  nrmmetd  21095  pi1grplem  21549  lmmbr2  21698  lmmbrf  21701  iscau2  21716  iscau4  21718  caucfil  21722  lmclim  21741  cfilucfil3OLD  21757  cfilucfil3  21758  bcthlem1  21763  bcth  21768  ishl2  21810  pmltpclem1  21860  elovolm  21886  ovolgelb  21891  ovolicc  21934  mbfaddlem  22067  i1fres  22112  mbfi1fseqlem4  22125  itg2l  22136  itg2leub  22141  itg2seq  22149  isibl  22172  iblitg  22175  dfitg  22176  itgeq2  22184  itgvallem  22191  iblcnlem1  22194  iblrelem  22197  iblpos  22199  ellimc3  22283  limciun  22298  limcun  22299  dvmptfsum  22376  dveflem  22380  lhop1lem  22414  dvfsumlem2  22428  dvfsumlem4  22430  mdegleb  22464  elply2  22593  plypf1  22609  coeval  22620  plydivlem4  22692  sincosq3sgn  22893  vmasum  23491  lgsqrlem1  23616  lgsquadlem1  23629  2sqlem8  23647  2sqlem9  23648  2sqlem11  23650  dchrisumlema  23673  dchrisumlem2  23675  pntibndlem3  23777  pntibnd  23778  pntleme  23793  pntlemp  23795  axtgsegcon  23861  axtg5seg  23862  axtgpasch  23864  iscgrg  23904  legov  23972  ltgov  23983  ishlg  23986  mirreu3  24035  israg  24074  islnopp  24113  ishpg  24128  iscgra  24169  brcgr  24203  brbtwn2  24208  colinearalg  24213  ax5seg  24241  axcontlem5  24271  axcontlem10  24276  usgraedg4  24387  cusgrafilem2  24480  cusgrafi  24482  uvtx01vtx  24492  usgrnloop  24565  spthonepeq  24589  usgra2adedgwlkonALT  24616  usgra2wlkspthlem1  24619  usgrcyclnl2  24641  4cycl4v4e  24666  4cycl4dv4e  24668  wwlk  24681  wlklniswwlkn2  24700  clwlkisclwwlklem0  24788  clwlkisclwwlk  24789  eleclclwwlkn  24833  usghashecclwwlk  24835  el2wlkonot  24869  el2spthonot  24870  el2spthonot0  24871  usg2spthonot  24888  usg2spthonot0  24889  usg2spthonot1  24890  isrusgra  24927  isrusgusrg  24932  isrgrac  24934  isrusgrac  24935  rusgranumwlkl1  24947  iseupa  24965  eupath2lem3  24979  1vwmgra  25003  3vfriswmgra  25005  3cyclfrgrarn1  25012  4cycl2vnunb  25017  vdn1frgrav2  25025  vdgn1frgrav2  25026  frgrancvvdeqlemB  25038  usg2spot2nb  25065  usgreg2spot  25067  2spotmdisj  25068  usgreghash2spot  25069  extwwlkfab  25090  numclwwlk2lem1  25102  numclwwlk5  25112  isgrpo  25198  isgrp2d  25237  isgrpda  25299  ismndo  25345  drngoi  25409  vci  25441  isvclem  25470  nmoofval  25677  nmooval  25678  nmosetn0  25680  nmoolb  25686  nmoubi  25687  nmoo0  25706  nmlno0lem  25708  isphg  25732  norm3lemt  26069  chlimi  26152  ocsh  26201  cmbr  26502  chscllem2  26556  spansncv  26571  eigorth  26757  nmopval  26775  nmopsetn0  26784  nmfnval  26795  nmfnsetn0  26797  nmoplb  26826  nmfnlb  26843  nmopnegi  26884  nmop0  26905  nmfn0  26906  nmlnop0iALT  26914  nmopun  26933  nmcexi  26945  branmfn  27024  leopmuli  27052  pjnmopi  27067  cvbr  27201  mdbr  27213  dmdbr  27218  atom1d  27272  chrelat2  27289  atcvati  27305  atord  27307  atcvat2  27308  chirredlem4  27312  mdsymlem5  27326  disjunsn  27453  opeldifid  27456  fcoinvbr  27461  fimarab  27483  fmptcof2  27502  ofpreima  27507  funcnv4mpt  27512  mpt2mptxf  27518  2ndpreima  27525  f1od2  27547  fpwrelmapffslem  27555  xeqlelt  27587  ishashinf  27606  ressprs  27643  isomnd  27691  archiabllem2a  27738  archiabl  27742  isslmd  27745  gsumle  27770  gsumvsca1  27773  gsumvsca2  27774  orngmul  27793  ismntop  28004  esumcvg  28092  sitgval  28274  eulerpartlemmf  28314  eulerpartlemgvv  28315  eulerpartlemn  28320  eulerpart  28321  brafs  28552  lgamgulmlem2  28572  erdszelem3  28637  erdsze  28646  pconcn  28669  cnpcon  28675  txpcon  28677  conpcon  28680  cvmscbv  28703  iscvm  28704  cvmsi  28710  cvmsval  28711  mclsval  28923  mclsppslem  28943  relexp0  29052  relexpsucr  29053  relexpsucl  29055  relexpadd  29061  relexpindlem  29062  elima4  29209  dfrdg2  29228  dfrdg3  29229  elpred  29257  trpredrec  29321  poseq  29333  soseq  29334  sltval  29407  nocvxminlem  29450  nofulllem1  29462  elfuns  29565  brimg  29587  brsuccf  29591  dfrdg4  29600  tfrqfree  29601  brofs  29655  funtransport  29681  fvtransport  29682  brifs  29693  lineext  29726  brfs  29729  btwnconn1lem11  29747  btwnconn1lem14  29750  brsegle  29758  segletr  29764  segleantisym  29765  seglelin  29766  funray  29790  fvray  29791  funline  29792  fvline  29794  ellines  29802  linethru  29803  ptrest  30048  mblfinlem3  30053  mblfinlem4  30054  ismblfin  30055  mbfresfi  30061  itg2addnclem  30066  itg2addnclem3  30068  itg2addnc  30069  ftc1anclem7  30096  ftc1anc  30098  areacirclem5  30111  trer  30134  opnrebl2  30139  nn0prpwlem  30140  isfne4  30158  isfne2  30160  isfne3  30161  unirep  30203  fnopabeqd  30210  fdc  30238  fdc1  30239  istotbnd  30265  heibor1lem  30305  heibor  30317  isriscg  30387  iscringd  30396  isidlc  30412  prtlem16  30610  prtlem15  30616  ismrcd1  30630  ismrcd2  30631  mzpcompact2lem  30684  eldioph  30691  eldioph2  30695  eldioph2b  30696  eldioph3  30699  diophin  30706  diophun  30707  diophrex  30709  rexrabdioph  30727  fphpd  30750  fphpdo  30751  pellexlem3  30767  monotuz  30877  monotoddzzfi  30878  monotoddzz  30879  oddcomabszz  30880  jm2.27  30950  rmydioph  30956  expdiophlem1  30963  expdiophlem2  30964  aomclem6  31005  aomclem8  31007  islssfg  31016  islssfg2  31017  hbtlem2  31073  hbtlem4  31075  hbtlem5  31077  hbtlem6  31078  dgraaval  31093  flcidc  31123  dvgrat  31193  cvgdvgrat  31194  lcmval  31198  lcmneg  31209  lcmgcdlem  31212  lcmass  31218  binomcxplemnotnn0  31261  2sbc6g  31322  2sbc5g  31323  iotasbc2  31327  pm14.122a  31329  pm14.123a  31332  monoords  31496  fperiodmullem  31503  fsumclf  31567  fsumsplitf  31568  fsummulc1f  31569  fsumnncl  31572  fsumsplit1  31573  fmul01  31574  fmuldfeqlem1  31576  fmuldfeq  31577  fmul01lt1lem1  31578  fmul01lt1lem2  31579  fproddivf  31588  fprodsplitf  31589  fprodsplit1f  31593  fprodexp  31600  fprodabs2  31602  climmulf  31610  climexp  31611  climsuse  31614  climrecf  31615  climinff  31617  climaddf  31621  mullimc  31622  limcdm0  31624  climf  31628  mullimcf  31629  constlimc  31630  idlimc  31632  limcperiod  31634  sumnnodd  31636  clim2f  31642  limcleqr  31650  neglimc  31653  addlimc  31654  0ellimcdiv  31655  cncfshift  31676  cncfperiod  31681  icccncfext  31690  fprodcncf  31704  fperdvper  31715  ioodvbdlimc1lem2  31729  ioodvbdlimc2lem  31731  dvmptmulf  31734  dvnmptdivc  31735  dvnmul  31740  dvmptfprod  31742  dvnprodlem1  31743  dvnprodlem2  31744  iblspltprt  31772  itgspltprt  31778  stoweidlem3  31785  stoweidlem4  31786  stoweidlem7  31789  stoweidlem15  31797  stoweidlem16  31798  stoweidlem17  31799  stoweidlem19  31801  stoweidlem20  31802  stoweidlem22  31804  stoweidlem23  31805  stoweidlem27  31809  stoweidlem30  31812  stoweidlem32  31814  stoweidlem34  31816  stoweidlem42  31824  stoweidlem43  31825  stoweidlem48  31830  stoweidlem51  31833  stoweidlem59  31841  stoweidlem60  31842  dirkercncflem2  31886  fourierdlem2  31891  fourierdlem3  31892  fourierdlem11  31900  fourierdlem12  31901  fourierdlem15  31904  fourierdlem16  31905  fourierdlem21  31910  fourierdlem34  31923  fourierdlem41  31930  fourierdlem42  31931  fourierdlem46  31935  fourierdlem48  31937  fourierdlem49  31938  fourierdlem50  31939  fourierdlem51  31940  fourierdlem54  31943  fourierdlem68  31957  fourierdlem71  31960  fourierdlem72  31961  fourierdlem73  31962  fourierdlem76  31965  fourierdlem79  31968  fourierdlem81  31970  fourierdlem83  31972  fourierdlem86  31975  fourierdlem87  31976  fourierdlem89  31978  fourierdlem90  31979  fourierdlem91  31980  fourierdlem92  31981  fourierdlem94  31983  fourierdlem97  31986  fourierdlem103  31992  fourierdlem104  31993  fourierdlem107  31996  fourierdlem111  32000  fourierdlem112  32001  fourierdlem113  32002  etransclem2  32019  etransclem46  32063  2reu4a  32194  isfusgracl  32426  rngcinv  32789  rngcinvOLD  32801  ringcinv  32840  ringcinvOLD  32864  opeliun2xp  32922  mpt2mptx2  32924  lcoval  33013  lco0  33028  islinindfis  33050  snlindsntor  33072  bnj976  33836  bnj852  33979  bnj1014  34018  bnj1015  34019  bnj1118  34040  bnj1123  34042  bnj1148  34052  bnj1171  34056  bnj1373  34086  bnj1489  34112  bj-eleq2w  34423  bj-finsumval0  34663  fsumshftd  34682  fsumshftdOLD  34683  lsmsat  34733  lsmsatcv  34735  islshpat  34742  lcvfbr  34745  lcvbr  34746  lsatcv0  34756  islshpkrN  34845  cvrval  34994  cvrval2  34999  cvrnbtwn2  35000  cvlexch1  35053  hlsuprexch  35105  cvrval5  35139  cvrat  35146  cvrat42  35168  3dim0  35181  3dim2  35192  islpln3  35257  islpln5  35259  islvol3  35300  islvol5  35303  4atlem11  35333  lineset  35462  isline  35463  ispsubsp2  35470  isline2  35498  isline3  35500  elpaddat  35528  elpadd2at  35530  dalawlem15  35609  pclfinclN  35674  4atex  35800  4atex2  35801  4atex3  35805  ltrnu  35845  cdleme0nex  36015  cdleme31so  36105  cdleme31fv  36116  cdleme31fv2  36119  cdlemefrs29pre00  36121  cdlemefrs29cpre1  36124  cdlemftr3  36291  cdlemb3  36332  cdlemg6d  36347  cdlemg33b  36433  cdlemg33c  36434  cdlemg33e  36436  cdlemk42  36667  dvhopellsm  36844  dibelval3  36874  diblsmopel  36898  diclspsn  36921  dihval  36959  dihopelvalcpre  36975  dih1dimatlem  37056  dihglb2  37069  dochkrshp3  37115  dihjatcclem4  37148  dihjat1lem  37155  mapdval  37355  mapdpglem30  37429  bj-ifbi3  37701  dfhe3  37799
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371
  Copyright terms: Public domain W3C validator