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  1604  drsb1  2497  eleq1w  2821  eleq1d  2823  clelab  2884  rexeqfOLD  3352  rmoeq1OLD  3415  reueq1OLD  3416  rmoeq1f  3420  rabeq  3447  rabeqbidva  3449  rabeqd  3462  rabeqf  3469  cgsex4gOLD  3526  vtocl2gafOLD  3579  vtocl4gaOLD  3586  alexeqg  3650  reu2eqd  3744  sbc2or  3799  sbc5ALT  3819  rexss  4070  psstr  4116  difin2  4306  r19.28z  4503  dfif6  4533  rabsneq  4648  rexreusng  4683  reurexprg  4708  rabsnifsb  4726  ssunsn2  4831  preq12bg  4857  opeq1  4877  eluni  4914  csbuni  4940  unissb  4943  iuneq12d  5025  disjxun  5145  unopab  5229  mpteq12da  5232  mpteq12f  5235  mpteq12dva  5236  dftr2c  5267  axrep1  5285  axreplem  5286  zfrepclf  5296  axsepgfromrep  5299  axsepg  5302  zfauscl  5303  reusv2lem4  5406  rabxfrd  5422  opthg  5487  otthg  5495  copsexgw  5500  copsexg  5501  opeqsng  5512  euotd  5522  elopabw  5535  pocl  5604  xpeq1  5702  elxpi  5710  vtoclr  5751  opbrop  5785  dmopab2rex  5930  resopab2  6055  dflim2  6442  dffun2  6572  fun11  6641  feq2  6717  f1eq2  6800  f1eq3  6801  foeq2  6817  brprcneu  6896  brprcneuALT  6897  ssimaexg  6994  dmfco  7004  fndmdif  7061  respreima  7085  isoeq5  7340  isoini  7357  isopolem  7364  f1oiso  7370  f1oiso2  7371  imaeqsexvOLD  7382  riotaeqdv  7388  oprabidw  7461  oprabid  7462  oprabv  7492  mpoeq123  7504  mpoeq123dva  7506  0mpo0  7515  eloprabga  7540  eloprabgaOLD  7541  resoprab  7550  resoprab2  7551  elrnmpores  7570  ov  7576  ov3  7595  ov6g  7596  ovg  7597  imaeqexov  7670  caoftrn  7736  uniuni  7780  limuni3  7872  elxp4  7944  elxp5  7945  opabex3d  7988  opabex3rd  7989  opabex3  7990  releldmdifi  8068  opiota  8082  eloprabi  8086  mptmpoopabbrd  8103  mptmpoopabbrdOLD  8104  mptmpoopabbrdOLDOLD  8106  cnvf1o  8134  frxp  8149  xporderlem  8150  poxp  8151  fnwelem  8154  poxp2  8166  xpord3pred  8175  poseq  8181  soseq  8182  suppimacnv  8197  rexsupp  8205  mpocurryd  8292  smoel2  8401  omeu  8621  oeeui  8638  omabs  8687  omopth  8698  eldifsucnn  8700  qliftel  8838  brecop  8848  eroveu  8850  erov  8852  ecopovtrn  8858  ixpsnf1o  8976  dom2lem  9030  mapsnend  9074  xpsnen  9093  xpassen  9104  pw2f1olem  9114  xpf1o  9177  unxpdom  9286  domunfican  9358  preleqALT  9654  zfinf  9676  cantnfs  9703  brttrcl  9750  ttrclselem2  9763  tcvalg  9775  r0weon  10049  fseqenlem1  10061  acni2  10083  aceq1  10154  aceq0  10155  dfac5lem4  10163  dfac2a  10167  dfac12lem2  10182  cardcf  10289  cfeq0  10293  cfsuc  10294  cff1  10295  cfss  10302  isf32lem5  10394  fin1a2lem6  10442  zfac  10497  brdom7disj  10568  brdom6disj  10569  axrepnd  10631  axunndlem1  10632  axinfnd  10643  axacndlem5  10648  axacnd  10649  zfcndrep  10651  zfcndinf  10655  zfcndac  10656  pwfseqlem4a  10698  pwfseqlem4  10699  gruina  10855  grothomex  10866  ordpipq  10979  elnpi  11025  genpass  11046  ltprord  11067  reclem2pr  11085  reclem3pr  11086  recexpr  11088  addsrmo  11110  mulsrmo  11111  addsrpr  11112  mulsrpr  11113  ltsosr  11131  mulgt0sr  11142  supsr  11149  ltresr  11177  axpre-lttrn  11203  axpre-mulgt0  11205  prime  12696  peano5uzti  12705  rexuz  12937  ltxr  13154  qbtwnre  13237  xmulneg1  13307  supxr2  13352  ixxval  13391  fzval  13545  preduz  13686  nn0opth2  14307  hashbclem  14487  hashf1lem2  14491  eqwrd  14591  pfxeq  14730  wrd2ind  14757  cshwcsh2id  14863  eqwrds3  14996  cleq1lem  15017  rtrclreclem3  15095  rtrclreclem4  15096  relexpindlem  15098  abslt  15349  absle  15350  lenegsq  15355  abs2difabs  15369  ello12  15548  elo12  15559  o1lo1  15569  rlimuni  15582  lo1resb  15596  o1resb  15598  2clim  15604  rlimcn3  15622  climcn2  15625  addcn2  15626  mulcn2  15628  o1of2  15645  sumeq1  15721  fsum2dlem  15802  modfsummod  15826  prodeq1f  15938  prodeq1  15939  fprod2dlem  16012  nndivdvds  16295  divalg2  16438  smupval  16521  gcdval  16529  gcdass  16580  lcmval  16625  lcmass  16647  rpexp  16755  pythagtriplem2  16850  pythagtrip  16867  vdwapun  17007  0ram  17053  ramub1lem2  17060  pwsle  17538  imasleval  17587  ismre  17634  ismri  17675  iscatd2  17725  dfiso2  17819  isssc  17867  funcpropd  17953  fullpropd  17973  fthres2b  17983  fthres2c  17984  setcsect  18142  cat1lem  18149  cat1  18150  prslem  18354  drsdir  18359  posi  18374  tosso  18476  odudlatb  18582  ipoval  18587  ipolt  18592  dirge  18660  gsumpropd2lem  18704  mgmhmpropd  18723  issgrpv  18746  issgrpn0  18747  ismhm0  18815  mhmpropd  18817  mndind  18853  mgmnsgrpex  18956  issubg3  19174  isga  19321  symgfixelq  19465  psgnfval  19532  psgnval  19539  dprdw  20044  subgdmdprd  20068  isrnghm  20457  issubrg  20587  resrhm2b  20618  rngcsect  20652  rngcinv  20653  ringcsect  20686  ringcinv  20687  drngpropd  20785  islmod  20878  lmodlema  20879  lmodprop2d  20938  lsslss  20976  lbspropd  21115  lbsacsbs  21175  znleval  21590  islbs4  21869  islinds3  21871  aspval2  21935  psrbag  21954  pf1ind  22374  mdetunilem4  22636  mdetunilem9  22641  istopg  22916  basis2  22973  tg2  22987  iscld  23050  isnei  23126  isneip  23128  neiptoptop  23154  neiptopnei  23155  neitr  23203  restlp  23206  iscn  23258  cnpval  23259  iscnp  23260  regsep  23357  1stcclb  23467  2ndc1stc  23474  2ndcctbss  23478  2ndcdisj  23479  llyi  23497  nllyi  23498  hausmapdom  23523  locfinnei  23546  comppfsc  23555  elkgen  23559  txbas  23590  txcls  23627  txcnpi  23631  ptpjopn  23635  txdis1cn  23658  txtube  23663  txcmplem1  23664  hausdiag  23668  tx1stc  23673  txkgen  23675  xkococn  23683  elqtop  23720  kqreglem1  23764  elmptrab  23850  isfbas  23852  elflim2  23987  elflim  23994  hauspwpwf1  24010  alexsublem  24067  ghmcnp  24138  qustgplem  24144  tsmssubm  24166  elutop  24257  ustuqtop4  24268  isucn  24302  iscfilu  24312  ispsmet  24329  ismet  24348  isxmet  24349  ismet2  24358  imasdsf1olem  24398  blres  24456  elmopn  24467  mopni  24520  neibl  24529  nrmmetd  24602  ngppropd  24665  elcncf  24928  mulc1cncf  24944  elpi1  25091  isclmp  25143  metcld2  25354  pmltpclem1  25496  itg1climres  25763  itg2val  25777  isibl  25814  itgeq1f  25820  itgeq1fOLD  25821  itgeq1  25822  cbvitgv  25826  itgresr  25828  iblcn  25848  itgfsum  25876  dvreslem  25958  dvfsumlem2  26081  dvfsumlem2OLD  26082  deg1ldg  26145  vieta1  26368  ulm2  26442  sincosq2sgn  26555  sincosq4sgn  26557  efopn  26714  dvdsflsumcom  27245  fsumvma2  27272  logfac2  27275  dchrptlem1  27322  lgsdchrval  27412  2lgslem1a  27449  pntibndlem3  27650  pntlemi  27662  pntleme  27666  pnt3  27670  sltval  27706  nolt02o  27754  slelttr  27816  nocvxminlem  27836  madebday  27952  sltlpss  27959  addsprop  28023  mulsproplemcbv  28155  mulsproplem1  28156  mulsprop  28170  absslt  28287  istrkgld  28481  istrkg2ld  28482  istrkg3ld  28483  axtgsegcon  28486  axtg5seg  28487  axtgpasch  28489  axtgupdim2  28493  legov  28607  islnopp  28761  ishpg  28781  iscgra1  28832  dfcgra2  28852  dfcgrg2  28885  brcgr  28929  brbtwn2  28934  axsegconlem1  28946  axsegcon  28956  axcontlem10  29002  edgssv2  29229  uhgr2edg  29239  isfusgrf1  29351  edgnbusgreu  29398  cplgr3v  29466  vtxdun  29513  upgr2wlk  29700  upgrtrls  29733  upgristrl  29734  upgrf1istrl  29735  2pthnloop  29763  usgr2pth  29796  isclwlke  29809  isclwlkupgr  29810  iswwlksnx  29869  wlknewwlksn  29916  2pthon3v  29972  elwwlks2on  29988  wpthswwlks2on  29990  rusgrnumwwlkl1  29997  rusgrnumwwlkb0  30000  clwwlknp  30065  clwwlkf  30075  erclwwlknsym  30098  erclwwlkntr  30099  clwwlknonwwlknonb  30134  0trl  30150  0spth  30154  0crct  30161  0cycl  30162  upgr4cycl4dv4e  30213  upgriseupth  30235  eupth2lem2  30247  3cyclfrgrrn1  30313  4cycl2vnunb  30318  frgrncvvdeqlem2  30328  frgr2wwlk1  30357  fusgr2wsp2nb  30362  numclwlk1lem1  30397  vciOLD  30589  isvclem  30605  nmoofval  30790  isph  30850  norm3lemt  31180  isch2  31251  cmbr  31612  eigre  31863  eigorth  31866  nmopub  31936  nmfnleub  31953  cvbr  32310  mdbr  32322  dmdbr  32327  chrelat2  32398  mdsymlem2  32432  rexunirn  32519  ifeqeqx  32562  iunrnmptss  32585  funcnvmpt  32683  fdifsupp  32699  ressupprn  32704  1stpreima  32721  fpwrelmapffslem  32749  isomnd  33060  archirng  33177  isslmd  33190  slmdlema  33191  urpropd  33221  orngmul  33312  lindflbs  33386  islbs5  33387  lindfpropd  33389  opprqus0g  33497  idlsrgval  33510  ressply1mon1p  33572  ccfldextdgrr  33696  constrsslem  33745  constrconj  33749  dya2iocuni  34264  omsfval  34275  elcarsg  34286  itgeq12dv  34307  isrrvv  34424  reprinrn  34611  reprdifc  34620  istrkg2d  34659  axtgupdim2ALTV  34661  brafs  34665  bnj956  34768  bnj1146  34783  bnj18eq1  34919  axsepg2  35074  axsepg2ALT  35075  zltp1ne  35093  isacycgr  35129  kur14  35200  pconncn  35208  cnpconn  35214  txpconn  35216  cvmscbv  35242  cvmcov  35247  cvmsi  35249  cvmsval  35250  cvmopnlem  35262  cvmlift2lem10  35296  cvmlift3lem2  35304  cvmlift3lem6  35308  cvmlift3lem7  35309  cvmlift3lem9  35311  cvmlift3  35312  satf0op  35361  sat1el2xp  35363  satffunlem  35385  dmopab3rexdif  35389  mclsssvlem  35546  mclsind  35554  rexxfr3dALT  35623  eldm3  35740  opelco3  35755  dfon2lem6  35769  dfon2lem7  35770  dfon2lem8  35771  dfon2  35773  elfuns  35896  brsuccf  35922  brofs  35986  5segofs  35987  brifs  36024  ifscgr  36025  brcolinear  36040  lineext  36057  brfs  36060  fscgr  36061  linecgr  36062  btwnconn1lem4  36071  btwnconn1lem8  36075  btwnconn1lem11  36078  btwnconn1lem12  36079  segcon2  36086  brsegle  36089  outsideofeq  36111  funray  36121  funline  36123  fvline  36125  linethru  36134  disjeq12dv  36197  prodeq12sdv  36200  itgeq12sdv  36201  cbvitgvw2  36230  cbvitgdavw  36263  cbvitgdavw2  36279  trer  36298  finminlem  36300  ivthALT  36317  filnetlem4  36363  knoppndvlem21  36514  bj-zfauscl  36906  bj-elgab  36921  bj-imdirvallem  37162  csboprabg  37312  topdifinffinlem  37329  icoreval  37335  isbasisrelowllem1  37337  isbasisrelowllem2  37338  relowlssretop  37345  pibp19  37396  wl-ax11-lem8  37572  curf  37584  ptrest  37605  poimirlem1  37607  poimirlem13  37619  poimirlem14  37620  poimirlem22  37628  poimirlem24  37630  poimirlem26  37632  poimirlem27  37633  heicant  37641  mblfinlem3  37645  mblfinlem4  37646  mbfresfi  37652  itg2addnclem3  37659  itg2addnc  37660  itg2gt0cn  37661  areacirclem5  37698  cover2  37701  cover2g  37702  fdc  37731  fdc1  37732  heibor1  37796  bfp  37810  rngosn3  37910  drngoi  37937  isdrngo1  37942  isriscg  37970  isfldidl2  38055  brressn  38422  islshpat  38998  lcvbr  39002  lshpsmreu  39090  ldual1dim  39147  cvrval  39250  cvrnbtwn3  39257  iscvlat2N  39305  ishlat3N  39335  hlrelat5N  39383  3dim0  39439  llnexatN  39503  islpln5  39517  islvol5  39561  pmapjat1  39835  ltrnu  40103  cdleme02N  40204  cdlemg33b  40689  cdlemg33c  40690  dvhb1dimN  40968  dibelval3  41129  dibopelval3  41130  dib1dim  41147  dibglbN  41148  diblsmopel  41153  dicval  41158  dicopelval  41159  dicelval3  41162  dicelval1sta  41169  dihopelvalcpre  41230  dih1dimatlem  41311  dihpN  41318  dihjatcclem4  41403  lpolsetN  41464  mapdpglem3  41657  hdmapglem7a  41909  sticksstones23  42150  exfinfldd  42184  fimgmcyclem  42519  fimgmcyc  42520  fsuppind  42576  fsuppssindlem2  42578  prjspeclsp  42598  mrefg2  42694  mzpclval  42712  eldiophb  42744  eldioph2lem1  42747  eldioph3  42753  lzenom  42757  diophin  42759  eldiophss  42761  diophrex  42762  eq0rabdioph  42763  pellexlem3  42818  elpell1qr  42834  elpell14qr  42836  elpell1234qr  42838  jm2.27  42996  rmydioph  43002  expdiophlem1  43009  expdioph  43011  pw2f1ocnv  43025  hbtlem1  43111  hbtlem7  43113  dgraalem  43133  dgraaub  43136  dflim7  43262  omabs2  43321  tfsconcatfv2  43329  tfsconcat0i  43334  nadd1suc  43381  ifpbi2  43456  inintabd  43568  cnvcnvintabd  43589  cnvintabd  43592  clcnvlem  43612  iunrelexpmin1  43697  uneqsn  44014  k0004lem2  44137  mnuprdlem1  44267  mnuprdlem2  44268  binomcxplemnotnn0  44351  2sbc6g  44410  2sbc5g  44411  iotasbc  44414  dropab1  44442  dropab2  44443  modelaxreplem3  44944  cbvmpo1  45037  r19.28zf  45101  disjinfi  45134  dmrelrnrel  45168  mullimc  45571  mullimcf  45578  limsuppnfd  45657  limsuppnf  45666  limsupre2  45680  limsupre2mpt  45685  limsupre3  45688  limsupre3mpt  45689  limsupre3uzlem  45690  fourierdlem42  46104  fourierdlem48  46109  fourierdlem50  46111  fourierdlem51  46112  fourierdlem54  46115  fourierdlem86  46147  ovnval2  46500  ovnsubaddlem1  46525  hoiqssbl  46580  vonicclem2  46639  f1cof1b  47026  f1ocof1ob2  47031  funressnbrafv2  47193  dfatdmfcoafv2  47203  2ffzoeq  47276  fundcmpsurbijinj  47334  ichreuopeq  47397  prproropf1olem4  47430  prprspr2  47442  prprsprreu  47443  prprreueq  47444  reuopreuprim  47450  isubgrgrim  47834  grtriprop  47845  isgrtri  47847  rngcsectALTV  48118  rngcinvALTV  48119  ringcsectALTV  48152  ringcinvALTV  48153  lmod1  48337  elbigo2  48401  rrx2vlinest  48590  i0oii  48715  io1ii  48716  lubeldm2d  48754  glbeldm2d  48755  functhinc  48844  fullthinc  48845