Theorem anbi1d 631

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  632  anbi1  633  pm5.71  1029  cador  1609  drsb1  2499  eleq1w  2819  eleq1d  2821  clelab  2880  rexeqfOLD  3327  rmoeq1OLD  3383  reueq1OLD  3384  rmoeq1f  3389  rabeq  3413  rabeqbidva  3415  rabeqd  3427  rabeqf  3433  cgsex4gOLD  3488  vtocl2gafOLD  3535  vtocl4gaOLD  3542  alexeqg  3605  reu2eqd  3694  sbc2or  3749  sbc5ALT  3769  rexssOLD  4011  psstr  4059  difin2  4253  r19.28z  4455  dfif6  4482  rabsneq  4599  rexreusng  4636  reurexprg  4661  rabsnifsb  4679  ssunsn2  4783  preq12bg  4809  opeq1  4829  eluni  4866  csbuni  4893  unissb  4896  iuneq12d  4976  disjxun  5096  unopab  5178  mpteq12da  5181  mpteq12f  5183  mpteq12dva  5184  dftr2c  5208  axrep1  5225  axreplem  5226  zfrepclf  5236  axsepgfromrep  5239  axsepg  5242  zfauscl  5243  reusv2lem4  5346  rabxfrd  5362  opthg  5425  otthg  5433  copsexgw  5438  copsexg  5439  opeqsng  5451  euotd  5461  elopabw  5474  pocl  5540  xpeq1  5638  elxpi  5646  vtoclr  5687  opbrop  5722  dmopab2rex  5866  resopab2  5995  rnco  6210  dflim2  6375  dffun2  6502  fun11  6566  feq2  6641  f1eq2  6726  f1eq3  6727  foeq2  6743  brprcneu  6824  brprcneuALT  6825  ssimaexg  6920  dmfco  6930  fndmdif  6987  respreima  7011  isoeq5  7267  isoini  7284  isopolem  7291  f1oiso  7297  f1oiso2  7298  imaeqsexvOLD  7309  riotaeqdv  7316  oprabidw  7389  oprabid  7390  oprabv  7418  mpoeq123  7430  mpoeq123dva  7432  0mpo0  7441  eloprabga  7467  resoprab  7476  resoprab2  7477  elrnmpores  7496  ov  7502  ov3  7521  ov6g  7522  ovg  7523  imaeqexov  7596  caoftrn  7663  uniuni  7707  limuni3  7794  elxp4  7864  elxp5  7865  opabex3d  7909  opabex3rd  7910  opabex3  7911  releldmdifi  7989  opiota  8003  eloprabi  8007  mptmpoopabbrd  8024  mptmpoopabbrdOLD  8025  cnvf1o  8053  frxp  8068  xporderlem  8069  poxp  8070  fnwelem  8073  poxp2  8085  xpord3pred  8094  poseq  8100  soseq  8101  suppimacnv  8116  rexsupp  8124  mpocurryd  8211  smoel2  8295  omeu  8512  oeeui  8530  omabs  8579  omopth  8590  eldifsucnn  8592  qliftel  8737  brecop  8747  eroveu  8749  erov  8751  ecopovtrn  8757  ixpsnf1o  8876  dom2lem  8929  mapsnend  8973  xpsnen  8989  xpassen  8999  pw2f1olem  9009  xpf1o  9067  unxpdom  9159  domunfican  9222  preleqALT  9526  zfinf  9548  cantnfs  9575  brttrcl  9622  ttrclselem2  9635  tcvalg  9645  r0weon  9922  fseqenlem1  9934  acni2  9956  aceq1  10027  aceq0  10028  dfac5lem4  10036  dfac2a  10040  dfac12lem2  10055  cardcf  10162  cfeq0  10166  cfsuc  10167  cff1  10168  cfss  10175  isf32lem5  10267  fin1a2lem6  10315  zfac  10370  brdom7disj  10441  brdom6disj  10442  axrepnd  10505  axunndlem1  10506  axinfnd  10517  axacndlem5  10522  axacnd  10523  zfcndrep  10525  zfcndinf  10529  zfcndac  10530  pwfseqlem4a  10572  pwfseqlem4  10573  gruina  10729  grothomex  10740  ordpipq  10853  elnpi  10899  genpass  10920  ltprord  10941  reclem2pr  10959  reclem3pr  10960  recexpr  10962  addsrmo  10984  mulsrmo  10985  addsrpr  10986  mulsrpr  10987  ltsosr  11005  mulgt0sr  11016  supsr  11023  ltresr  11051  axpre-lttrn  11077  axpre-mulgt0  11079  prime  12573  peano5uzti  12582  rexuz  12811  ltxr  13029  qbtwnre  13114  xmulneg1  13184  supxr2  13229  ixxval  13269  fzval  13425  preduz  13566  nn0opth2  14195  hashbclem  14375  hashf1lem2  14379  eqwrd  14480  pfxeq  14619  wrd2ind  14646  cshwcsh2id  14751  eqwrds3  14884  cleq1lem  14905  rtrclreclem3  14983  rtrclreclem4  14984  relexpindlem  14986  abslt  15238  absle  15239  lenegsq  15244  abs2difabs  15258  ello12  15439  elo12  15450  o1lo1  15460  rlimuni  15473  lo1resb  15487  o1resb  15489  2clim  15495  rlimcn3  15513  climcn2  15516  addcn2  15517  mulcn2  15519  o1of2  15536  sumeq1  15612  fsum2dlem  15693  modfsummod  15717  prodeq1f  15829  prodeq1  15830  fprod2dlem  15903  nndivdvds  16188  divalg2  16332  smupval  16415  gcdval  16423  gcdass  16474  lcmval  16519  lcmass  16541  rpexp  16649  pythagtriplem2  16745  pythagtrip  16762  vdwapun  16902  0ram  16948  ramub1lem2  16955  pwsle  17413  imasleval  17462  ismre  17509  ismri  17554  iscatd2  17604  dfiso2  17696  isssc  17744  funcpropd  17826  fullpropd  17846  fthres2b  17856  fthres2c  17857  setcsect  18013  cat1lem  18020  cat1  18021  prslem  18220  drsdir  18225  posi  18240  tosso  18340  odudlatb  18448  ipoval  18453  ipolt  18458  dirge  18526  gsumpropd2lem  18604  mgmhmpropd  18623  issgrpv  18646  issgrpn0  18647  ismhm0  18715  mhmpropd  18717  mndind  18753  mgmnsgrpex  18856  issubg3  19074  isga  19220  symgfixelq  19362  psgnfval  19429  psgnval  19436  dprdw  19941  subgdmdprd  19965  isomnd  20052  isrnghm  20377  issubrg  20504  resrhm2b  20535  rngcsect  20569  rngcinv  20570  ringcsect  20603  ringcinv  20604  drngpropd  20702  orngmul  20798  islmod  20815  lmodlema  20816  lmodprop2d  20875  lsslss  20912  lbspropd  21051  lbsacsbs  21111  znleval  21509  islbs4  21787  islinds3  21789  aspval2  21854  psrbag  21873  pf1ind  22299  mdetunilem4  22559  mdetunilem9  22564  istopg  22839  basis2  22895  tg2  22909  iscld  22971  isnei  23047  isneip  23049  neiptoptop  23075  neiptopnei  23076  neitr  23124  restlp  23127  iscn  23179  cnpval  23180  iscnp  23181  regsep  23278  1stcclb  23388  2ndc1stc  23395  2ndcctbss  23399  2ndcdisj  23400  llyi  23418  nllyi  23419  hausmapdom  23444  locfinnei  23467  comppfsc  23476  elkgen  23480  txbas  23511  txcls  23548  txcnpi  23552  ptpjopn  23556  txdis1cn  23579  txtube  23584  txcmplem1  23585  hausdiag  23589  tx1stc  23594  txkgen  23596  xkococn  23604  elqtop  23641  kqreglem1  23685  elmptrab  23771  isfbas  23773  elflim2  23908  elflim  23915  hauspwpwf1  23931  alexsublem  23988  ghmcnp  24059  qustgplem  24065  tsmssubm  24087  elutop  24177  ustuqtop4  24188  isucn  24221  iscfilu  24231  ispsmet  24248  ismet  24267  isxmet  24268  ismet2  24277  imasdsf1olem  24317  blres  24375  elmopn  24386  mopni  24436  neibl  24445  nrmmetd  24518  ngppropd  24581  elcncf  24838  mulc1cncf  24854  elpi1  25001  isclmp  25053  metcld2  25263  pmltpclem1  25405  itg1climres  25671  itg2val  25685  isibl  25722  itgeq1f  25728  itgeq1fOLD  25729  itgeq1  25730  cbvitgv  25734  itgresr  25736  iblcn  25756  itgfsum  25784  dvreslem  25866  dvfsumlem2  25989  dvfsumlem2OLD  25990  deg1ldg  26053  vieta1  26276  ulm2  26350  sincosq2sgn  26464  sincosq4sgn  26466  efopn  26623  dvdsflsumcom  27154  fsumvma2  27181  logfac2  27184  dchrptlem1  27231  lgsdchrval  27321  2lgslem1a  27358  pntibndlem3  27559  pntlemi  27571  pntleme  27575  pnt3  27579  ltsval  27615  nolt02o  27663  leltstr  27729  nocvxminlem  27750  madebday  27896  ltslpss  27904  addsprop  27972  mulsproplemcbv  28111  mulsproplem1  28112  mulsprop  28126  abslts  28245  eucliddivs  28372  bdayfinbndlem2  28464  z12sge0  28479  istrkgld  28531  istrkg2ld  28532  istrkg3ld  28533  axtgsegcon  28536  axtg5seg  28537  axtgpasch  28539  axtgupdim2  28543  legov  28657  islnopp  28811  ishpg  28831  iscgra1  28882  dfcgra2  28902  dfcgrg2  28935  brcgr  28973  brbtwn2  28978  axsegconlem1  28990  axsegcon  29000  axcontlem10  29046  edgssv2  29271  uhgr2edg  29281  isfusgrf1  29393  edgnbusgreu  29440  cplgr3v  29508  vtxdun  29555  upgr2wlk  29740  upgrtrls  29773  upgristrl  29774  upgrf1istrl  29775  dfpth2  29802  2pthnloop  29804  usgr2pth  29837  isclwlke  29850  isclwlkupgr  29851  iswwlksnx  29913  wlknewwlksn  29960  2pthon3v  30016  elwwlks2on  30034  wpthswwlks2on  30037  rusgrnumwwlkl1  30044  rusgrnumwwlkb0  30047  clwwlknp  30112  clwwlkf  30122  erclwwlknsym  30145  erclwwlkntr  30146  clwwlknonwwlknonb  30181  0trl  30197  0spth  30201  0crct  30208  0cycl  30209  upgr4cycl4dv4e  30260  upgriseupth  30282  eupth2lem2  30294  3cyclfrgrrn1  30360  4cycl2vnunb  30365  frgrncvvdeqlem2  30375  frgr2wwlk1  30404  fusgr2wsp2nb  30409  numclwlk1lem1  30444  vciOLD  30636  isvclem  30652  nmoofval  30837  isph  30897  norm3lemt  31227  isch2  31298  cmbr  31659  eigre  31910  eigorth  31913  nmopub  31983  nmfnleub  32000  cvbr  32357  mdbr  32369  dmdbr  32374  chrelat2  32445  mdsymlem2  32479  rexunirn  32566  ifeqeqx  32617  iunrnmptss  32640  funcnvmpt  32745  fdifsupp  32764  ressupprn  32769  1stpreima  32786  fpwrelmapffslem  32811  archirng  33270  isslmd  33284  slmdlema  33285  urpropd  33313  lindflbs  33460  islbs5  33461  lindfpropd  33463  opprqus0g  33571  idlsrgval  33584  ressply1mon1p  33649  ccfldextdgrr  33829  constrsslem  33898  constrconj  33902  constrlccllem  33910  constrcbvlem  33912  dya2iocuni  34440  omsfval  34451  elcarsg  34462  itgeq12dv  34483  isrrvv  34600  reprinrn  34775  reprdifc  34784  istrkg2d  34823  axtgupdim2ALTV  34825  brafs  34829  bnj956  34932  bnj1146  34947  bnj18eq1  35083  axsepg2  35238  axsepg2ALT  35239  zltp1ne  35304  isacycgr  35339  kur14  35410  pconncn  35418  cnpconn  35424  txpconn  35426  cvmscbv  35452  cvmcov  35457  cvmsi  35459  cvmsval  35460  cvmopnlem  35472  cvmlift2lem10  35506  cvmlift3lem2  35514  cvmlift3lem6  35518  cvmlift3lem7  35519  cvmlift3lem9  35521  cvmlift3  35522  satf0op  35571  sat1el2xp  35573  satffunlem  35595  dmopab3rexdif  35599  mclsssvlem  35756  mclsind  35764  rexxfr3dALT  35833  eldm3  35955  opelco3  35969  dfon2lem6  35980  dfon2lem7  35981  dfon2lem8  35982  dfon2  35984  elfuns  36107  lemsuccf  36133  brofs  36199  5segofs  36200  brifs  36237  ifscgr  36238  brcolinear  36253  lineext  36270  brfs  36273  fscgr  36274  linecgr  36275  btwnconn1lem4  36284  btwnconn1lem8  36288  btwnconn1lem11  36291  btwnconn1lem12  36292  segcon2  36299  brsegle  36302  outsideofeq  36324  funray  36334  funline  36336  fvline  36338  linethru  36347  disjeq12dv  36409  prodeq12sdv  36412  itgeq12sdv  36413  cbvitgvw2  36442  cbvitgdavw  36475  cbvitgdavw2  36491  trer  36510  finminlem  36512  ivthALT  36529  filnetlem4  36575  knoppndvlem21  36732  bj-zfauscl  37125  bj-elgab  37140  bj-imdirvallem  37385  csboprabg  37535  topdifinffinlem  37552  icoreval  37558  isbasisrelowllem1  37560  isbasisrelowllem2  37561  relowlssretop  37568  pibp19  37619  curf  37799  ptrest  37820  poimirlem1  37822  poimirlem13  37834  poimirlem14  37835  poimirlem22  37843  poimirlem24  37845  poimirlem26  37847  poimirlem27  37848  heicant  37856  mblfinlem3  37860  mblfinlem4  37861  mbfresfi  37867  itg2addnclem3  37874  itg2addnc  37875  itg2gt0cn  37876  areacirclem5  37913  cover2  37916  cover2g  37917  fdc  37946  fdc1  37947  heibor1  38011  bfp  38025  rngosn3  38125  drngoi  38152  isdrngo1  38157  isriscg  38185  isfldidl2  38270  eldmxrncnvepres  38619  brressn  38704  islshpat  39277  lcvbr  39281  lshpsmreu  39369  ldual1dim  39426  cvrval  39529  cvrnbtwn3  39536  iscvlat2N  39584  ishlat3N  39614  hlrelat5N  39661  3dim0  39717  llnexatN  39781  islpln5  39795  islvol5  39839  pmapjat1  40113  ltrnu  40381  cdleme02N  40482  cdlemg33b  40967  cdlemg33c  40968  dvhb1dimN  41246  dibelval3  41407  dibopelval3  41408  dib1dim  41425  dibglbN  41426  diblsmopel  41431  dicval  41436  dicopelval  41437  dicelval3  41440  dicelval1sta  41447  dihopelvalcpre  41508  dih1dimatlem  41589  dihpN  41596  dihjatcclem4  41681  lpolsetN  41742  mapdpglem3  41935  hdmapglem7a  42187  sticksstones23  42423  exfinfldd  42457  fimgmcyclem  42788  fimgmcyc  42789  fsuppind  42833  fsuppssindlem2  42835  prjspeclsp  42855  mrefg2  42949  mzpclval  42967  eldiophb  42999  eldioph2lem1  43002  eldioph3  43008  lzenom  43012  diophin  43014  eldiophss  43016  diophrex  43017  eq0rabdioph  43018  pellexlem3  43073  elpell1qr  43089  elpell14qr  43091  elpell1234qr  43093  jm2.27  43250  rmydioph  43256  expdiophlem1  43263  expdioph  43265  pw2f1ocnv  43279  hbtlem1  43365  hbtlem7  43367  dgraalem  43387  dgraaub  43390  dflim7  43515  omabs2  43574  tfsconcatfv2  43582  tfsconcat0i  43587  nadd1suc  43634  ifpbi2  43708  inintabd  43820  cnvcnvintabd  43841  cnvintabd  43844  clcnvlem  43864  iunrelexpmin1  43949  uneqsn  44266  k0004lem2  44389  mnuprdlem1  44513  mnuprdlem2  44514  binomcxplemnotnn0  44597  2sbc6g  44656  2sbc5g  44657  iotasbc  44660  dropab1  44687  dropab2  44688  relpeq5  45189  modelaxreplem3  45221  omssaxinf2  45229  brpermmodel  45244  permaxinf2lem  45253  cbvmpo1  45342  r19.28zf  45403  disjinfi  45436  dmrelrnrel  45470  mullimc  45862  mullimcf  45869  limsuppnfd  45946  limsuppnf  45955  limsupre2  45969  limsupre2mpt  45974  limsupre3  45977  limsupre3mpt  45978  limsupre3uzlem  45979  fourierdlem42  46393  fourierdlem48  46398  fourierdlem50  46400  fourierdlem51  46401  fourierdlem54  46404  fourierdlem86  46436  ovnval2  46789  ovnsubaddlem1  46814  hoiqssbl  46869  vonicclem2  46928  f1cof1b  47323  f1ocof1ob2  47328  funressnbrafv2  47490  dfatdmfcoafv2  47500  2ffzoeq  47573  fundcmpsurbijinj  47656  ichreuopeq  47719  prproropf1olem4  47752  prprspr2  47764  prprsprreu  47765  prprreueq  47766  reuopreuprim  47772  isubgrgrim  48175  grtriprop  48187  isgrtri  48189  opgpgvtx  48301  pgnbgreunbgrlem1  48359  pgnbgreunbgrlem4  48365  grlimedgnedg  48377  rngcsectALTV  48521  rngcinvALTV  48522  ringcsectALTV  48555  ringcinvALTV  48556  lmod1  48738  elbigo2  48798  rrx2vlinest  48987  eloprab1st2nd  49113  i0oii  49165  io1ii  49166  lubeldm2d  49203  glbeldm2d  49204  sectpropdlem  49281  invpropdlem  49283  isopropdlem  49285  uppropd  49426  functhinc  49693  fullthinc  49695