Theorem anbi1d 632

Description: Deduction adding a right 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
anbid.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
anbi1d	⊢ (𝜑 → ((𝜓 ∧ 𝜃) ↔ (𝜒 ∧ 𝜃)))

Proof of Theorem anbi1d

Step	Hyp	Ref	Expression
1		anbid.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	a1d 25	. 2 ⊢ (𝜑 → (𝜃 → (𝜓 ↔ 𝜒)))
3	2	pm5.32rd 578	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) ↔ (𝜒 ∧ 𝜃)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  anbi12d  633  anbi1  634  pm5.71  1030  cador  1610  drsb1  2499  eleq1w  2819  eleq1d  2821  clelab  2880  rmoeq1f  3379  rabeq  3403  rabeqbidva  3405  rabeqd  3417  rabeqf  3423  vtocl2gafOLD  3523  vtocl4gaOLD  3530  alexeqg  3593  reu2eqd  3682  sbc2or  3737  sbc5ALT  3757  rexssOLD  3999  psstr  4047  difin2  4241  r19.28z  4442  dfif6  4469  rabsneq  4586  rexreusng  4623  reurexprg  4648  rabsnifsb  4666  ssunsn2  4770  preq12bg  4796  opeq1  4816  eluni  4853  csbuni  4880  unissb  4883  iuneq12d  4963  disjxun  5083  unopab  5165  mpteq12da  5168  mpteq12f  5170  mpteq12dva  5171  dftr2c  5195  axrep1  5213  axreplem  5214  zfrepclf  5226  axsepgfromrep  5229  axsepg  5232  zfauscl  5233  reusv2lem4  5343  rabxfrd  5359  opthg  5430  otthg  5438  copsexgw  5443  copsexgwOLD  5444  copsexg  5445  opeqsng  5457  euotd  5467  elopabw  5481  pocl  5547  xpeq1  5645  elxpi  5653  vtoclr  5694  opbrop  5729  dmopab2rex  5872  resopab2  6001  rnco  6216  dflim2  6381  dffun2  6508  fun11  6572  feq2  6647  f1eq2  6732  f1eq3  6733  foeq2  6749  brprcneu  6830  brprcneuALT  6831  ssimaexg  6926  dmfco  6936  funcnvmpt  6949  fndmdif  6994  respreima  7018  isoeq5  7276  isoini  7293  isopolem  7300  f1oiso  7306  f1oiso2  7307  imaeqsexvOLD  7318  riotaeqdv  7325  oprabidw  7398  oprabid  7399  oprabv  7427  mpoeq123  7439  mpoeq123dva  7441  0mpo0  7450  eloprabga  7476  resoprab  7485  resoprab2  7486  elrnmpores  7505  ov  7511  ov3  7530  ov6g  7531  ovg  7532  imaeqexov  7605  caoftrn  7672  uniuni  7716  limuni3  7803  elxp4  7873  elxp5  7874  opabex3d  7918  opabex3rd  7919  opabex3  7920  releldmdifi  7998  opiota  8012  eloprabi  8016  mptmpoopabbrd  8033  cnvf1o  8061  frxp  8076  xporderlem  8077  poxp  8078  fnwelem  8081  poxp2  8093  xpord3pred  8102  poseq  8108  soseq  8109  suppimacnv  8124  rexsupp  8132  mpocurryd  8219  smoel2  8303  omeu  8520  oeeui  8538  omabs  8587  omopth  8598  eldifsucnn  8600  qliftel  8747  brecop  8757  eroveu  8759  erov  8761  ecopovtrn  8767  ixpsnf1o  8886  dom2lem  8939  mapsnend  8983  xpsnen  8999  xpassen  9009  pw2f1olem  9019  xpf1o  9077  unxpdom  9169  domunfican  9232  preleqALT  9538  zfinf  9560  cantnfs  9587  brttrcl  9634  ttrclselem2  9647  tcvalg  9657  r0weon  9934  fseqenlem1  9946  acni2  9968  aceq1  10039  aceq0  10040  dfac5lem4  10048  dfac2a  10052  dfac12lem2  10067  cardcf  10174  cfeq0  10178  cfsuc  10179  cff1  10180  cfss  10187  isf32lem5  10279  fin1a2lem6  10327  zfac  10382  brdom7disj  10453  brdom6disj  10454  axrepnd  10517  axunndlem1  10518  axinfnd  10529  axacndlem5  10534  axacnd  10535  zfcndrep  10537  zfcndinf  10541  zfcndac  10542  pwfseqlem4a  10584  pwfseqlem4  10585  gruina  10741  grothomex  10752  ordpipq  10865  elnpi  10911  genpass  10932  ltprord  10953  reclem2pr  10971  reclem3pr  10972  recexpr  10974  addsrmo  10996  mulsrmo  10997  addsrpr  10998  mulsrpr  10999  ltsosr  11017  mulgt0sr  11028  supsr  11035  ltresr  11063  axpre-lttrn  11089  axpre-mulgt0  11091  prime  12610  peano5uzti  12619  rexuz  12848  ltxr  13066  qbtwnre  13151  xmulneg1  13221  supxr2  13266  ixxval  13306  fzval  13463  preduz  13604  nn0opth2  14234  hashbclem  14414  hashf1lem2  14418  eqwrd  14519  pfxeq  14658  wrd2ind  14685  cshwcsh2id  14790  eqwrds3  14923  cleq1lem  14944  rtrclreclem3  15022  rtrclreclem4  15023  relexpindlem  15025  abslt  15277  absle  15278  lenegsq  15283  abs2difabs  15297  ello12  15478  elo12  15489  o1lo1  15499  rlimuni  15512  lo1resb  15526  o1resb  15528  2clim  15534  rlimcn3  15552  climcn2  15555  addcn2  15556  mulcn2  15558  o1of2  15575  sumeq1  15651  fsum2dlem  15732  modfsummod  15757  prodeq1f  15871  prodeq1  15872  fprod2dlem  15945  nndivdvds  16230  divalg2  16374  smupval  16457  gcdval  16465  gcdass  16516  lcmval  16561  lcmass  16583  rpexp  16692  pythagtriplem2  16788  pythagtrip  16805  vdwapun  16945  0ram  16991  ramub1lem2  16998  pwsle  17456  imasleval  17505  ismre  17552  ismri  17597  iscatd2  17647  dfiso2  17739  isssc  17787  funcpropd  17869  fullpropd  17889  fthres2b  17899  fthres2c  17900  setcsect  18056  cat1lem  18063  cat1  18064  prslem  18263  drsdir  18268  posi  18283  tosso  18383  odudlatb  18491  ipoval  18496  ipolt  18501  dirge  18569  gsumpropd2lem  18647  mgmhmpropd  18666  issgrpv  18689  issgrpn0  18690  ismhm0  18758  mhmpropd  18760  mndind  18796  mgmnsgrpex  18902  issubg3  19120  isga  19266  symgfixelq  19408  psgnfval  19475  psgnval  19482  dprdw  19987  subgdmdprd  20011  isomnd  20098  isrnghm  20421  issubrg  20548  resrhm2b  20579  rngcsect  20613  rngcinv  20614  ringcsect  20647  ringcinv  20648  drngpropd  20746  orngmul  20842  islmod  20859  lmodlema  20860  lmodprop2d  20919  lsslss  20956  lbspropd  21094  lbsacsbs  21154  znleval  21534  islbs4  21812  islinds3  21814  aspval2  21878  psrbag  21897  pf1ind  22320  mdetunilem4  22580  mdetunilem9  22585  istopg  22860  basis2  22916  tg2  22930  iscld  22992  isnei  23068  isneip  23070  neiptoptop  23096  neiptopnei  23097  neitr  23145  restlp  23148  iscn  23200  cnpval  23201  iscnp  23202  regsep  23299  1stcclb  23409  2ndc1stc  23416  2ndcctbss  23420  2ndcdisj  23421  llyi  23439  nllyi  23440  hausmapdom  23465  locfinnei  23488  comppfsc  23497  elkgen  23501  txbas  23532  txcls  23569  txcnpi  23573  ptpjopn  23577  txdis1cn  23600  txtube  23605  txcmplem1  23606  hausdiag  23610  tx1stc  23615  txkgen  23617  xkococn  23625  elqtop  23662  kqreglem1  23706  elmptrab  23792  isfbas  23794  elflim2  23929  elflim  23936  hauspwpwf1  23952  alexsublem  24009  ghmcnp  24080  qustgplem  24086  tsmssubm  24108  elutop  24198  ustuqtop4  24209  isucn  24242  iscfilu  24252  ispsmet  24269  ismet  24288  isxmet  24289  ismet2  24298  imasdsf1olem  24338  blres  24396  elmopn  24407  mopni  24457  neibl  24466  nrmmetd  24539  ngppropd  24602  elcncf  24856  mulc1cncf  24872  elpi1  25012  isclmp  25064  metcld2  25274  pmltpclem1  25415  itg1climres  25681  itg2val  25695  isibl  25732  itgeq1f  25738  itgeq1fOLD  25739  itgeq1  25740  cbvitgv  25744  itgresr  25746  iblcn  25766  itgfsum  25794  dvreslem  25876  dvfsumlem2  25994  deg1ldg  26057  vieta1  26278  ulm2  26350  sincosq2sgn  26463  sincosq4sgn  26465  efopn  26622  dvdsflsumcom  27151  fsumvma2  27177  logfac2  27180  dchrptlem1  27227  lgsdchrval  27317  2lgslem1a  27354  pntibndlem3  27555  pntlemi  27567  pntleme  27571  pnt3  27575  ltsval  27611  nolt02o  27659  leltstr  27725  nocvxminlem  27746  madebday  27892  ltslpss  27900  addsprop  27968  mulsproplemcbv  28107  mulsproplem1  28108  mulsprop  28122  abslts  28241  eucliddivs  28368  bdayfinbndlem2  28460  z12sge0  28475  istrkgld  28527  istrkg2ld  28528  istrkg3ld  28529  axtgsegcon  28532  axtg5seg  28533  axtgpasch  28535  axtgupdim2  28539  legov  28653  islnopp  28807  ishpg  28827  iscgra1  28878  dfcgra2  28898  dfcgrg2  28931  brcgr  28969  brbtwn2  28974  axsegconlem1  28986  axsegcon  28996  axcontlem10  29042  edgssv2  29267  uhgr2edg  29277  isfusgrf1  29389  edgnbusgreu  29436  cplgr3v  29504  vtxdun  29550  upgr2wlk  29735  upgrtrls  29768  upgristrl  29769  upgrf1istrl  29770  dfpth2  29797  2pthnloop  29799  usgr2pth  29832  isclwlke  29845  isclwlkupgr  29846  iswwlksnx  29908  wlknewwlksn  29955  2pthon3v  30011  elwwlks2on  30029  wpthswwlks2on  30032  rusgrnumwwlkl1  30039  rusgrnumwwlkb0  30042  clwwlknp  30107  clwwlkf  30117  erclwwlknsym  30140  erclwwlkntr  30141  clwwlknonwwlknonb  30176  0trl  30192  0spth  30196  0crct  30203  0cycl  30204  upgr4cycl4dv4e  30255  upgriseupth  30277  eupth2lem2  30289  3cyclfrgrrn1  30355  4cycl2vnunb  30360  frgrncvvdeqlem2  30370  frgr2wwlk1  30399  fusgr2wsp2nb  30404  numclwlk1lem1  30439  vciOLD  30632  isvclem  30648  nmoofval  30833  isph  30893  norm3lemt  31223  isch2  31294  cmbr  31655  eigre  31906  eigorth  31909  nmopub  31979  nmfnleub  31996  cvbr  32353  mdbr  32365  dmdbr  32370  chrelat2  32441  mdsymlem2  32475  rexunirn  32561  ifeqeqx  32612  iunrnmptss  32635  fdifsupp  32758  ressupprn  32763  1stpreima  32780  fpwrelmapffslem  32805  archirng  33249  isslmd  33263  slmdlema  33264  urpropd  33292  lindflbs  33439  islbs5  33440  lindfpropd  33442  opprqus0g  33550  idlsrgval  33563  ressply1mon1p  33628  ccfldextdgrr  33816  constrsslem  33885  constrconj  33889  constrlccllem  33897  constrcbvlem  33899  dya2iocuni  34427  omsfval  34438  elcarsg  34449  itgeq12dv  34470  isrrvv  34587  reprinrn  34762  reprdifc  34771  istrkg2d  34810  axtgupdim2ALTV  34812  brafs  34816  bnj956  34919  bnj1146  34933  bnj18eq1  35069  axsepg2  35225  axsepg2ALT  35226  zltp1ne  35292  isacycgr  35327  kur14  35398  pconncn  35406  cnpconn  35412  txpconn  35414  cvmscbv  35440  cvmcov  35445  cvmsi  35447  cvmsval  35448  cvmopnlem  35460  cvmlift2lem10  35494  cvmlift3lem2  35502  cvmlift3lem6  35506  cvmlift3lem7  35507  cvmlift3lem9  35509  cvmlift3  35510  satf0op  35559  sat1el2xp  35561  satffunlem  35583  dmopab3rexdif  35587  mclsssvlem  35744  mclsind  35752  rexxfr3dALT  35821  eldm3  35943  opelco3  35957  dfon2lem6  35968  dfon2lem7  35969  dfon2lem8  35970  dfon2  35972  elfuns  36095  lemsuccf  36121  brofs  36187  5segofs  36188  brifs  36225  ifscgr  36226  brcolinear  36241  lineext  36258  brfs  36261  fscgr  36262  linecgr  36263  btwnconn1lem4  36272  btwnconn1lem8  36276  btwnconn1lem11  36279  btwnconn1lem12  36280  segcon2  36287  brsegle  36290  outsideofeq  36312  funray  36322  funline  36324  fvline  36326  linethru  36335  disjeq12dv  36397  prodeq12sdv  36400  itgeq12sdv  36401  cbvitgvw2  36430  cbvitgdavw  36463  cbvitgdavw2  36479  trer  36498  finminlem  36500  ivthALT  36517  filnetlem4  36563  axtco1  36655  axtco1from2  36657  ttcexg  36714  mh-infprim1bi  36728  knoppndvlem21  36792  bj-zfauscl  37231  bj-elgab  37246  bj-imdirvallem  37494  csboprabg  37646  topdifinffinlem  37663  icoreval  37669  isbasisrelowllem1  37671  isbasisrelowllem2  37672  relowlssretop  37679  pibp19  37730  curf  37919  ptrest  37940  poimirlem1  37942  poimirlem13  37954  poimirlem14  37955  poimirlem22  37963  poimirlem24  37965  poimirlem26  37967  poimirlem27  37968  heicant  37976  mblfinlem3  37980  mblfinlem4  37981  mbfresfi  37987  itg2addnclem3  37994  itg2addnc  37995  itg2gt0cn  37996  areacirclem5  38033  cover2  38036  cover2g  38037  fdc  38066  fdc1  38067  heibor1  38131  bfp  38145  rngosn3  38245  drngoi  38272  isdrngo1  38277  isriscg  38305  isfldidl2  38390  raldmqseu  38686  eldmxrncnvepres  38755  brressn  38852  islshpat  39463  lcvbr  39467  lshpsmreu  39555  ldual1dim  39612  cvrval  39715  cvrnbtwn3  39722  iscvlat2N  39770  ishlat3N  39800  hlrelat5N  39847  3dim0  39903  llnexatN  39967  islpln5  39981  islvol5  40025  pmapjat1  40299  ltrnu  40567  cdleme02N  40668  cdlemg33b  41153  cdlemg33c  41154  dvhb1dimN  41432  dibelval3  41593  dibopelval3  41594  dib1dim  41611  dibglbN  41612  diblsmopel  41617  dicval  41622  dicopelval  41623  dicelval3  41626  dicelval1sta  41633  dihopelvalcpre  41694  dih1dimatlem  41775  dihpN  41782  dihjatcclem4  41867  lpolsetN  41928  mapdpglem3  42121  hdmapglem7a  42373  sticksstones23  42608  exfinfldd  42642  fimgmcyclem  42978  fimgmcyc  42979  fsuppind  43023  fsuppssindlem2  43025  prjspeclsp  43045  mrefg2  43139  mzpclval  43157  eldiophb  43189  eldioph2lem1  43192  eldioph3  43198  lzenom  43202  diophin  43204  eldiophss  43206  diophrex  43207  eq0rabdioph  43208  pellexlem3  43259  elpell1qr  43275  elpell14qr  43277  elpell1234qr  43279  jm2.27  43436  rmydioph  43442  expdiophlem1  43449  expdioph  43451  pw2f1ocnv  43465  hbtlem1  43551  hbtlem7  43553  dgraalem  43573  dgraaub  43576  dflim7  43701  omabs2  43760  tfsconcatfv2  43768  tfsconcat0i  43773  nadd1suc  43820  ifpbi2  43894  inintabd  44006  cnvcnvintabd  44027  cnvintabd  44030  clcnvlem  44050  iunrelexpmin1  44135  uneqsn  44452  k0004lem2  44575  mnuprdlem1  44699  mnuprdlem2  44700  binomcxplemnotnn0  44783  2sbc6g  44842  2sbc5g  44843  iotasbc  44846  dropab1  44873  dropab2  44874  relpeq5  45375  modelaxreplem3  45407  omssaxinf2  45415  brpermmodel  45430  permaxinf2lem  45439  cbvmpo1  45528  r19.28zf  45589  disjinfi  45622  dmrelrnrel  45655  mullimc  46046  mullimcf  46053  limsuppnfd  46130  limsuppnf  46139  limsupre2  46153  limsupre2mpt  46158  limsupre3  46161  limsupre3mpt  46162  limsupre3uzlem  46163  fourierdlem42  46577  fourierdlem48  46582  fourierdlem50  46584  fourierdlem51  46585  fourierdlem54  46588  fourierdlem86  46620  ovnval2  46973  ovnsubaddlem1  46998  hoiqssbl  47053  vonicclem2  47112  f1cof1b  47525  f1ocof1ob2  47530  funressnbrafv2  47692  dfatdmfcoafv2  47702  2ffzoeq  47776  fundcmpsurbijinj  47870  ichreuopeq  47933  prproropf1olem4  47966  prprspr2  47978  prprsprreu  47979  prprreueq  47980  reuopreuprim  47986  nprmmul3  47989  isubgrgrim  48405  grtriprop  48417  isgrtri  48419  opgpgvtx  48531  pgnbgreunbgrlem1  48589  pgnbgreunbgrlem4  48595  grlimedgnedg  48607  rngcsectALTV  48751  rngcinvALTV  48752  ringcsectALTV  48785  ringcinvALTV  48786  lmod1  48968  elbigo2  49028  rrx2vlinest  49217  eloprab1st2nd  49343  i0oii  49395  io1ii  49396  lubeldm2d  49433  glbeldm2d  49434  sectpropdlem  49511  invpropdlem  49513  isopropdlem  49515  uppropd  49656  functhinc  49923  fullthinc  49925