Theorem imbi2d 316

Description: Deduction adding an antecedent to both sides of a logical equivalence. (Contributed by NM, 11-May-1993.)

Hypothesis

Ref	Expression
imbid.1

Assertion

Ref	Expression
imbi2d

Proof of Theorem imbi2d

Step	Hyp	Ref	Expression
1		imbid.1	. . 3
2	1	a1d 25	. 2
3	2	pm5.74d 247	1

Syntax hints:  ->wi 4  <->wb 184

This theorem is referenced by:  imbi12d  320  imbi2  324  pm5.42  548  orbi2d  701  con3th  958  ax12vOLD  1856  ax12v2  2083  axc14  2113  ax12eq  2271  ax12el  2272  ax12indalem  2275  ax12inda2ALT  2276  ax12inda  2278  ax12v2-o  2279  mo2  2293  2eu6OLD  2384  2gencl  3140  3gencl  3141  vtocl2gf  3169  vtocl3gf  3170  vtocl4g  3178  eqeu  3270  mo2icl  3278  euind  3286  reu7  3294  reuind  3303  sbctt  3398  sbcnestgf  3839  r19.36zv  3930  dedth2h  3994  dedth3h  3995  dedth4h  3996  preq12bg  4209  prel12g  4210  elint  4292  elintrabg  4299  intab  4317  trss  4554  axrep1  4564  axrep2  4565  axrep3  4566  bm1.3ii  4576  reusv3  4660  pocl  4812  swopolem  4814  solin  4828  freq1  4854  frminex  4864  vtoclr  5049  2optocl  5082  3optocl  5083  raliunxp  5147  resieq  5289  iss  5326  cnveqb  5467  funmo  5609  funimaexg  5670  fnbrfvb  5913  fvelimab  5929  fvmptss  5964  fmptco  6064  fprg  6080  fnressn  6083  fressnfv  6085  isoselem  6237  ovg  6441  caovcan  6479  caovordig  6480  caovord  6486  tfisi  6693  tfindsg  6695  tfinds2  6698  tfinds3  6699  dfom2  6702  elom  6703  findsg  6727  finds2  6728  f1o2ndf1  6908  poxp  6912  fnse  6917  smoeq  7040  smores  7042  smogt  7057  tfrlem1  7064  tfr3  7087  oaordi  7214  oeordi  7255  oeoa  7265  oeoe  7267  nnacl  7279  nnmcl  7280  nnecl  7281  nnacom  7285  nnaordi  7286  nnawordi  7289  nnaass  7290  nndi  7291  nnmass  7292  nnmsucr  7293  nnmcom  7294  nnmordi  7299  2ecoptocl  7421  3ecoptocl  7422  undifixp  7525  xpdom2g  7633  findcard2  7780  xpfi  7811  fnfi  7818  fodomfi  7819  finsschain  7847  marypha1lem  7913  marypha1  7914  supeq1  7925  ordiso2  7961  ordtypelem7  7970  wemaplem1  7992  inf3lem2  8067  inf3lem5  8070  infdiffi  8095  cantnfval2  8109  cantnfle  8111  cantnfp1lem3  8120  oemapval  8123  cantnflem1  8129  cantnf  8133  cantnfval2OLD  8139  cantnfleOLD  8141  cantnfp1lem3OLD  8146  cantnflem1OLD  8152  cantnfOLD  8155  wemapwe  8160  wemapweOLD  8161  cnfcom  8165  cnfcom3clem  8170  cnfcomOLD  8173  cnfcom3clemOLD  8178  tz9.1  8181  r1pwOLD  8285  cplem2  8329  karden  8334  infxpenc2lem2  8418  infxpenc2lem2OLD  8422  fseqenlem1  8426  dfac8clem  8434  alephinit  8497  dfac4  8524  dfac5lem5  8529  dfac2a  8531  dfac2  8532  dfacacn  8542  dfac12lem3  8546  kmlem2  8552  kmlem13  8563  ackbij1lem16  8636  sornom  8678  infpssrlem4  8707  fin23lem14  8734  fin23lem32  8745  fin23lem34  8747  fin23lem36  8749  isf32lem1  8754  isf32lem2  8755  axcc2lem  8837  axcc3  8839  axcclem  8858  zornn0g  8906  ttukeylem5  8914  ttukeylem6  8915  axrepnd  8990  axpowndlem3  8996  axpowndlem3OLD  8997  zfcndrep  9013  fpwwe2lem8  9036  pwfseqlem3  9059  wunr1om  9118  wunfi  9120  tskr1om  9166  ingru  9214  grudomon  9216  axgroth3  9230  axgroth4  9231  nqereu  9328  mulcanenq  9359  elnp  9386  elnpi  9387  prlem934  9432  infm3  10527  nnaddcl  10583  nnmulcl  10584  peano5uzi  10976  uzind2  10980  uzindOLD  10982  nn0indd  10986  zindd  10990  eluzadd  11138  uzaddcl  11166  uzwo  11173  uzwoOLD  11174  indstr  11179  zmax  11208  xmulasslem  11506  xrsupsslem  11527  xrinfmsslem  11528  xrsupss  11529  xrinfmss  11530  flval2  11950  om2uzlti  12061  uzrdgfni  12069  rabssnn0fi  12095  mptnn0fsupp  12103  seqcl2  12125  seqfveq2  12129  seqshft2  12133  monoord  12137  seqsplit  12140  seqcaopr3  12142  seqf1olem2a  12145  seqf1o  12148  seqid2  12153  seqhomo  12154  ser1const  12163  expcllem  12177  expeq0  12196  mulexp  12205  expadd  12208  expmul  12211  leexp2r  12223  leexp1a  12224  bernneq  12292  modexp  12301  facdiv  12365  faclbnd  12368  faclbnd4lem4  12374  faclbnd6  12377  hashgadd  12445  hashxp  12492  hashmap  12493  hashf1lem2  12505  hashf1  12506  seqcoll  12512  wrdind  12702  wrd2ind  12703  swrdccatin12lem3  12715  cshweqrep  12789  2cshwcshw  12793  cjexp  12983  absexp  13137  rlim  13318  rlim2  13319  rlim0  13331  rlim0lt  13332  rlimi  13336  ello12r  13340  ello1mpt  13344  ello1d  13346  elo12r  13351  lo1o1  13355  o1lo1  13360  lo1res  13382  climshft  13399  o1compt  13410  rlimo1  13439  lo1add  13449  lo1mul  13450  rlimdiv  13468  climub  13484  climserle  13485  caucvgrlem  13495  caurcvgr  13496  iseraltlem2  13505  summolem2a  13537  sumss  13546  fsum2d  13586  fsumabs  13615  fsumrlim  13625  fsumo1  13626  fsumiun  13635  binom  13642  bcxmas  13647  climcndslem1  13661  climcndslem2  13662  cvgrat  13692  clim2prod  13697  prodfn0  13703  prodfrec  13704  ntrivcvgfvn0  13708  prodmolem2a  13741  fprodabs  13778  fprodn0  13783  fprod2d  13785  fprodefsum  13830  demoivreALT  13936  ruclem8  13970  ruclem9  13971  dvdsle  14031  dvdsfac  14041  divalglem7  14057  bitsinv1  14092  sadcadd  14108  sadadd2  14110  saddisjlem  14114  smuval2  14132  smupvallem  14133  smu01lem  14135  smupval  14138  smueqlem  14140  smumullem  14142  bezoutlem4  14179  gcdmultiple  14188  rplpwr  14194  nn0seqcvgd  14199  seq1st  14200  alginv  14204  algcvga  14208  algfx  14209  prmind2  14228  prmdvdsexp  14255  prmfac1  14259  reumodprminv  14329  pcmpt  14411  pcfac  14418  prmpwdvds  14422  prmreclem4  14437  vdwlem10  14508  ramval  14526  ramcl  14547  cshwrepswhash1  14587  prmlem1a  14592  imasleval  14938  ismre  14987  mreexexd  15045  lubprop  15616  lublecllem  15618  glbprop  15629  joinlem  15641  meetlem  15655  isglbd  15747  lubun  15753  poslubmo  15776  posglbmo  15777  poslubd  15778  mrcmndind  15997  frmdgsum  16030  mulgnnass  16170  mhmmulg  16174  gsumwrev  16401  gsmsymgrfix  16453  gsmsymgreq  16457  psgnunilem3  16521  sylow1lem1  16618  efginvrel2  16745  efgsrel  16752  efgredlemd  16762  efgredlem  16765  efgred  16766  efgrelexlemb  16768  gsum2dlem2  16998  gsum2dOLD  17000  gsumcom2  17003  ablfac1eulem  17123  pgpfac1lem2  17126  pgpfac1lem5  17130  pgpfac1  17131  pgpfac  17135  srgmulgass  17182  srgpcomp  17183  srgbinom  17196  lmodvsmmulgdi  17547  isdomn2  17948  assamulgscm  17999  mplcoe1  18127  mplcoe3  18128  mplcoe3OLD  18129  mplcoe5  18131  mplcoe2OLD  18133  gsummoncoe1  18346  cnfldexp  18451  islindf4  18873  dmatval  18994  dmatel  18995  dmatmulcl  19002  pmatcoe1fsupp  19202  decpmataa0  19269  decpmatmulsumfsupp  19274  pmatcollpw2lem  19278  pm2mpmhmlem1  19319  fiinopn  19410  mretopd  19593  neiptoptop  19632  cnpfval  19735  iscnp3  19745  tgcn  19753  lmbr  19759  lmbr2  19760  lmbrf  19761  lmss  19799  ishaus  19823  hausnei2  19854  t1sep2  19870  fiuncmp  19904  dfcon2  19920  1stcfb  19946  2ndc1stc  19952  1stcrest  19954  1stcelcls  19962  1stccn  19964  lly1stc  19997  elkgen  20037  kgencn  20057  tx1stc  20151  xkopt  20156  cnmptcom  20179  isr0  20238  r0sep  20249  ptcmpfi  20314  isfildlem  20358  rnelfm  20454  fbflim  20477  flimrest  20484  isflf  20494  flffbas  20496  lmflf  20506  fclsrest  20525  isfcf  20535  cnextfvval  20565  tmdmulg  20591  tmdgsum  20594  eltsms  20631  tsmsi  20632  tsmsgsum  20637  tsmsgsumOLD  20640  tsmssubm  20644  tsmsresOLD  20645  tsmsres  20646  tsmsf1o  20647  isust  20706  isucn  20781  isucn2  20782  ucnima  20784  imasdsf1olem  20876  metss  21011  met1stc  21024  metcnp  21044  metcnpi  21047  metcnpi2  21048  metucnOLD  21091  metucn  21092  xrge0tsms  21339  fsumcn  21374  elcncf  21393  cncfi  21398  rescncf  21401  cncfco  21411  caucfil  21722  equivcau  21739  caubl  21746  caublcls  21747  ovolgelb  21891  ovolunlem1a  21907  ovolicc2lem3  21930  voliunlem1  21960  voliunlem3  21962  volsuplem  21965  volsup  21966  dyadmax  22007  vitali  22022  itg2leub  22141  itgfsum  22233  dvnadd  22332  dvnres  22334  cpnord  22338  dvnfre  22355  dvmptfsum  22376  dvferm1  22386  dvferm2  22388  rolle  22391  dvlip  22394  c1lip1  22398  lhop1  22415  deg1leb  22495  ply1divex  22537  fta1g  22568  plyco  22638  dgrcolem1  22670  dgrco  22672  dvnply2  22683  plydivex  22693  aalioulem2  22729  aalioulem3  22730  aalioulem5  22732  aaliou3lem2  22739  dvntaylp  22766  taylthlem1  22768  ulmdvlem3  22797  abelthlem9  22835  cxpmul2  23070  scvxcvx  23315  jensenlem2  23317  jensen  23318  wilthlem3  23344  perfectlem2  23505  bcmono  23552  bposlem5  23563  lgsquad2lem2  23634  dchrisumlem1  23674  dchrisum0flb  23695  pntpbnd1  23771  pntlemf  23790  qabvle  23810  qabvexp  23811  ostthlem2  23813  ostth2lem2  23819  sizeusglecusglem1  24484  2pthoncl  24605  fargshiftf1  24637  3v3e3cycl1  24644  4cycl4v4e  24666  4cycl4dv4e  24668  wlkiswwlk2lem4  24694  wlkiswwlk2  24697  clwlkisclwwlklem2a  24785  clwlkisclwwlklem2  24786  clwlkfoclwwlk  24845  el2wlkonot  24869  el2spthonot  24870  rusgranumwlk  24957  eupatrl  24968  eupath2  24980  frgra3vlem1  25000  3vfriswmgralem  25004  usg2spot2nb  25065  2spotmdisj  25068  numclwlk2lem2f1o  25105  isplig  25179  gxnn0add  25276  gxnn0mul  25279  ghgrpOLD  25370  ghabloOLD  25371  isnvlem  25503  nvi  25507  nmoubi  25687  nmounbi  25691  nmblolbi  25715  ipasslem1  25746  ipassi  25756  hlim2  26109  pjhth  26311  spansni  26475  elspansn2  26485  pjige0  26609  pjcjt2  26610  pjopyth  26638  elcnop  26776  elcnfn  26801  nmopub  26827  cnopc  26832  nmfnleub  26844  elnlfn  26847  cnfnc  26849  nmbdoplb  26944  nmcexi  26945  nmcoplb  26949  lnfnmul  26967  nmbdfnlb  26969  nmcfnlb  26973  pjss2coi  27083  pjssmi  27084  isst  27132  ishst  27133  stcltr1i  27193  mdbr  27213  dmdbr  27218  mddmd2  27228  mdslmd1lem3  27246  mdslmd1lem4  27247  elat2  27259  atcvat2  27308  cdj1i  27352  rmoeq  27386  iuninc  27428  fmptcof2  27502  nn0min  27611  isomnd  27691  omndadd  27696  isarchi2  27729  archirng  27732  archiexdiv  27734  archiabl  27742  xrge0tsmsd  27775  isorng  27789  ofldchr  27804  crefeq  27848  nexple  28005  esumfzf  28075  issiga  28111  isrnsiga  28113  ismeas  28170  isrnmeas  28171  measiun  28189  eulerpartlemn  28320  sseqp1  28334  rrvsum  28393  signsply0  28508  signstfvc  28531  subfacp1lem6  28629  erdszelem8  28642  isscon  28671  cvmliftlem7  28736  cvmliftlem10  28739  cvmlift3lem2  28765  mrsubvrs  28882  mclsssvlem  28922  mclsval  28923  mclsax  28929  mclsind  28930  ghomf1olem  29034  relexp0  29052  relexpsucr  29053  relexpsucl  29055  relexpind  29063  dfrtrclrec2  29066  rtrclreclem.refl  29067  rtrclreclem.subset  29068  rtrclreclem.min  29070  dfrtrcl2  29071  shftvalg  29115  iprodefisumlem  29123  binomfallfac  29163  faclimlem1  29168  dfpo2  29184  rdgprc  29227  preddowncl  29276  trpredmintr  29314  frmin  29322  soseq  29334  wfr3g  29342  wfrlem4  29346  frr3g  29386  bpolycl  29814  bpolydif  29817  fveleq  29916  wl-sblimt  29999  wl-sbhbt  30002  wl-2sb6d  30008  wl-mo2dnae  30019  wl-mo2t  30020  heicant  30049  mbfresfi  30061  itg2gt0cn  30070  sdclem2  30235  fdc  30238  seqpo  30240  incsequz  30241  mettrifi  30250  prdsbnd2  30291  heiborlem4  30310  bfplem1  30318  iscringd  30396  maxidlval  30436  igenval2  30463  ismrc  30633  incssnn0  30643  mzpexpmpt  30677  pell14qrexpclnn0  30802  monotuz  30877  expmordi  30883  rmxypos  30885  jm2.17a  30898  jm2.17b  30899  rmygeid  30902  divalgmodcl  30929  jm2.18  30930  jm2.19lem3  30933  jm2.25  30941  jm2.15nn0  30945  jm2.16nn0  30946  wepwsolem  30987  aomclem8  31007  dfac11  31008  pwslnm  31040  lnr2i  31065  hbtlem5  31077  cnsrexpcl  31114  rngunsnply  31122  isdomn3  31164  dvgrat  31193  pm14.122b  31330  fnchoice  31404  fperiodmullem  31503  fmul01  31574  fmuldfeq  31577  climsuselem1  31613  climinff  31617  ellimcabssub0  31623  limcleqr  31650  addlimc  31654  0ellimcdiv  31655  limclner  31657  dvnmptdivc  31735  dvnmptconst  31738  dvnmul  31740  iblspltprt  31772  itgspltprt  31778  stoweidlem2  31784  stoweidlem3  31785  stoweidlem17  31799  stoweidlem19  31801  stoweidlem21  31803  stoweidlem26  31808  fourierdlem42  31931  2ffzoeq  32341  usgra2pth  32354  usgfis  32446  lmodvsmdi  32975  dmatALTval  33001  dmatALTbasel  33003  snlindsntor  33072  ldepsnlinc  33109  bnj941  33831  bnj106  33926  bnj155  33937  bnj590  33968  bnj591  33969  bnj849  33983  bnj893  33986  bnj944  33996  bnj1128  34046  bj-con3thALT  34162  bj-axc15v  34330  bj-axrep1  34374  bj-axrep2  34375  bj-axrep3  34376  riotasvd  34687  isopos  34905  isat3  35032  ishlat1  35077  glbconN  35101  ispsubsp  35469  isldil  35834  isltrn  35843  isdilN  35879  trlval  35887  cdleme27b  36094  cdleme29b  36101  cdleme31sn1  36107  cdleme31sn1c  36114  cdleme40v  36195  cdlemk36  36639  cdlemkid5  36661  cdlemn11pre  36937  dihord2pre  36952  islpolN  37210  hdmapffval  37556  hdmapfval  37557  hdmapval2lem  37561  bj-ifbi23  37704

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