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  2497  eleq1w  2816  eleq1d  2818  clelab  2877  rexeqfOLD  3324  rmoeq1OLD  3380  reueq1OLD  3381  rmoeq1f  3386  rabeq  3410  rabeqbidva  3412  rabeqd  3424  rabeqf  3430  cgsex4gOLD  3485  vtocl2gafOLD  3532  vtocl4gaOLD  3539  alexeqg  3602  reu2eqd  3691  sbc2or  3746  sbc5ALT  3766  rexssOLD  4008  psstr  4056  difin2  4250  r19.28z  4452  dfif6  4479  rabsneq  4596  rexreusng  4633  reurexprg  4658  rabsnifsb  4676  ssunsn2  4780  preq12bg  4806  opeq1  4826  eluni  4863  csbuni  4890  unissb  4893  iuneq12d  4973  disjxun  5093  unopab  5175  mpteq12da  5178  mpteq12f  5180  mpteq12dva  5181  dftr2c  5205  axrep1  5222  axreplem  5223  zfrepclf  5233  axsepgfromrep  5236  axsepg  5239  zfauscl  5240  reusv2lem4  5343  rabxfrd  5359  opthg  5422  otthg  5430  copsexgw  5435  copsexg  5436  opeqsng  5448  euotd  5458  elopabw  5471  pocl  5537  xpeq1  5635  elxpi  5643  vtoclr  5684  opbrop  5719  dmopab2rex  5863  resopab2  5992  rnco  6207  dflim2  6372  dffun2  6499  fun11  6563  feq2  6638  f1eq2  6723  f1eq3  6724  foeq2  6740  brprcneu  6821  brprcneuALT  6822  ssimaexg  6917  dmfco  6927  fndmdif  6984  respreima  7008  isoeq5  7264  isoini  7281  isopolem  7288  f1oiso  7294  f1oiso2  7295  imaeqsexvOLD  7306  riotaeqdv  7313  oprabidw  7386  oprabid  7387  oprabv  7415  mpoeq123  7427  mpoeq123dva  7429  0mpo0  7438  eloprabga  7464  resoprab  7473  resoprab2  7474  elrnmpores  7493  ov  7499  ov3  7518  ov6g  7519  ovg  7520  imaeqexov  7593  caoftrn  7660  uniuni  7704  limuni3  7791  elxp4  7861  elxp5  7862  opabex3d  7906  opabex3rd  7907  opabex3  7908  releldmdifi  7986  opiota  8000  eloprabi  8004  mptmpoopabbrd  8021  mptmpoopabbrdOLD  8022  cnvf1o  8050  frxp  8065  xporderlem  8066  poxp  8067  fnwelem  8070  poxp2  8082  xpord3pred  8091  poseq  8097  soseq  8098  suppimacnv  8113  rexsupp  8121  mpocurryd  8208  smoel2  8292  omeu  8509  oeeui  8526  omabs  8575  omopth  8586  eldifsucnn  8588  qliftel  8733  brecop  8743  eroveu  8745  erov  8747  ecopovtrn  8753  ixpsnf1o  8872  dom2lem  8925  mapsnend  8969  xpsnen  8985  xpassen  8995  pw2f1olem  9005  xpf1o  9063  unxpdom  9154  domunfican  9217  preleqALT  9518  zfinf  9540  cantnfs  9567  brttrcl  9614  ttrclselem2  9627  tcvalg  9637  r0weon  9914  fseqenlem1  9926  acni2  9948  aceq1  10019  aceq0  10020  dfac5lem4  10028  dfac2a  10032  dfac12lem2  10047  cardcf  10154  cfeq0  10158  cfsuc  10159  cff1  10160  cfss  10167  isf32lem5  10259  fin1a2lem6  10307  zfac  10362  brdom7disj  10433  brdom6disj  10434  axrepnd  10496  axunndlem1  10497  axinfnd  10508  axacndlem5  10513  axacnd  10514  zfcndrep  10516  zfcndinf  10520  zfcndac  10521  pwfseqlem4a  10563  pwfseqlem4  10564  gruina  10720  grothomex  10731  ordpipq  10844  elnpi  10890  genpass  10911  ltprord  10932  reclem2pr  10950  reclem3pr  10951  recexpr  10953  addsrmo  10975  mulsrmo  10976  addsrpr  10977  mulsrpr  10978  ltsosr  10996  mulgt0sr  11007  supsr  11014  ltresr  11042  axpre-lttrn  11068  axpre-mulgt0  11070  prime  12564  peano5uzti  12573  rexuz  12802  ltxr  13020  qbtwnre  13105  xmulneg1  13175  supxr2  13220  ixxval  13260  fzval  13416  preduz  13557  nn0opth2  14186  hashbclem  14366  hashf1lem2  14370  eqwrd  14471  pfxeq  14610  wrd2ind  14637  cshwcsh2id  14742  eqwrds3  14875  cleq1lem  14896  rtrclreclem3  14974  rtrclreclem4  14975  relexpindlem  14977  abslt  15229  absle  15230  lenegsq  15235  abs2difabs  15249  ello12  15430  elo12  15441  o1lo1  15451  rlimuni  15464  lo1resb  15478  o1resb  15480  2clim  15486  rlimcn3  15504  climcn2  15507  addcn2  15508  mulcn2  15510  o1of2  15527  sumeq1  15603  fsum2dlem  15684  modfsummod  15708  prodeq1f  15820  prodeq1  15821  fprod2dlem  15894  nndivdvds  16179  divalg2  16323  smupval  16406  gcdval  16414  gcdass  16465  lcmval  16510  lcmass  16532  rpexp  16640  pythagtriplem2  16736  pythagtrip  16753  vdwapun  16893  0ram  16939  ramub1lem2  16946  pwsle  17404  imasleval  17453  ismre  17500  ismri  17545  iscatd2  17595  dfiso2  17687  isssc  17735  funcpropd  17817  fullpropd  17837  fthres2b  17847  fthres2c  17848  setcsect  18004  cat1lem  18011  cat1  18012  prslem  18211  drsdir  18216  posi  18231  tosso  18331  odudlatb  18439  ipoval  18444  ipolt  18449  dirge  18517  gsumpropd2lem  18595  mgmhmpropd  18614  issgrpv  18637  issgrpn0  18638  ismhm0  18706  mhmpropd  18708  mndind  18744  mgmnsgrpex  18847  issubg3  19065  isga  19211  symgfixelq  19353  psgnfval  19420  psgnval  19427  dprdw  19932  subgdmdprd  19956  isomnd  20043  isrnghm  20368  issubrg  20495  resrhm2b  20526  rngcsect  20560  rngcinv  20561  ringcsect  20594  ringcinv  20595  drngpropd  20693  orngmul  20789  islmod  20806  lmodlema  20807  lmodprop2d  20866  lsslss  20903  lbspropd  21042  lbsacsbs  21102  znleval  21500  islbs4  21778  islinds3  21780  aspval2  21845  psrbag  21864  pf1ind  22290  mdetunilem4  22550  mdetunilem9  22555  istopg  22830  basis2  22886  tg2  22900  iscld  22962  isnei  23038  isneip  23040  neiptoptop  23066  neiptopnei  23067  neitr  23115  restlp  23118  iscn  23170  cnpval  23171  iscnp  23172  regsep  23269  1stcclb  23379  2ndc1stc  23386  2ndcctbss  23390  2ndcdisj  23391  llyi  23409  nllyi  23410  hausmapdom  23435  locfinnei  23458  comppfsc  23467  elkgen  23471  txbas  23502  txcls  23539  txcnpi  23543  ptpjopn  23547  txdis1cn  23570  txtube  23575  txcmplem1  23576  hausdiag  23580  tx1stc  23585  txkgen  23587  xkococn  23595  elqtop  23632  kqreglem1  23676  elmptrab  23762  isfbas  23764  elflim2  23899  elflim  23906  hauspwpwf1  23922  alexsublem  23979  ghmcnp  24050  qustgplem  24056  tsmssubm  24078  elutop  24168  ustuqtop4  24179  isucn  24212  iscfilu  24222  ispsmet  24239  ismet  24258  isxmet  24259  ismet2  24268  imasdsf1olem  24308  blres  24366  elmopn  24377  mopni  24427  neibl  24436  nrmmetd  24509  ngppropd  24572  elcncf  24829  mulc1cncf  24845  elpi1  24992  isclmp  25044  metcld2  25254  pmltpclem1  25396  itg1climres  25662  itg2val  25676  isibl  25713  itgeq1f  25719  itgeq1fOLD  25720  itgeq1  25721  cbvitgv  25725  itgresr  25727  iblcn  25747  itgfsum  25775  dvreslem  25857  dvfsumlem2  25980  dvfsumlem2OLD  25981  deg1ldg  26044  vieta1  26267  ulm2  26341  sincosq2sgn  26455  sincosq4sgn  26457  efopn  26614  dvdsflsumcom  27145  fsumvma2  27172  logfac2  27175  dchrptlem1  27222  lgsdchrval  27312  2lgslem1a  27349  pntibndlem3  27550  pntlemi  27562  pntleme  27566  pnt3  27570  sltval  27606  nolt02o  27654  slelttr  27716  nocvxminlem  27737  madebday  27865  sltlpss  27873  addsprop  27939  mulsproplemcbv  28074  mulsproplem1  28075  mulsprop  28089  absslt  28207  eucliddivs  28321  zs12ge0  28413  istrkgld  28457  istrkg2ld  28458  istrkg3ld  28459  axtgsegcon  28462  axtg5seg  28463  axtgpasch  28465  axtgupdim2  28469  legov  28583  islnopp  28737  ishpg  28757  iscgra1  28808  dfcgra2  28828  dfcgrg2  28861  brcgr  28899  brbtwn2  28904  axsegconlem1  28916  axsegcon  28926  axcontlem10  28972  edgssv2  29197  uhgr2edg  29207  isfusgrf1  29319  edgnbusgreu  29366  cplgr3v  29434  vtxdun  29481  upgr2wlk  29666  upgrtrls  29699  upgristrl  29700  upgrf1istrl  29701  dfpth2  29728  2pthnloop  29730  usgr2pth  29763  isclwlke  29776  isclwlkupgr  29777  iswwlksnx  29839  wlknewwlksn  29886  2pthon3v  29942  elwwlks2on  29960  wpthswwlks2on  29963  rusgrnumwwlkl1  29970  rusgrnumwwlkb0  29973  clwwlknp  30038  clwwlkf  30048  erclwwlknsym  30071  erclwwlkntr  30072  clwwlknonwwlknonb  30107  0trl  30123  0spth  30127  0crct  30134  0cycl  30135  upgr4cycl4dv4e  30186  upgriseupth  30208  eupth2lem2  30220  3cyclfrgrrn1  30286  4cycl2vnunb  30291  frgrncvvdeqlem2  30301  frgr2wwlk1  30330  fusgr2wsp2nb  30335  numclwlk1lem1  30370  vciOLD  30562  isvclem  30578  nmoofval  30763  isph  30823  norm3lemt  31153  isch2  31224  cmbr  31585  eigre  31836  eigorth  31839  nmopub  31909  nmfnleub  31926  cvbr  32283  mdbr  32295  dmdbr  32300  chrelat2  32371  mdsymlem2  32405  rexunirn  32492  ifeqeqx  32543  iunrnmptss  32566  funcnvmpt  32671  fdifsupp  32690  ressupprn  32695  1stpreima  32712  fpwrelmapffslem  32739  archirng  33198  isslmd  33212  slmdlema  33213  urpropd  33241  lindflbs  33388  islbs5  33389  lindfpropd  33391  opprqus0g  33499  idlsrgval  33512  ressply1mon1p  33577  ccfldextdgrr  33757  constrsslem  33826  constrconj  33830  constrlccllem  33838  constrcbvlem  33840  dya2iocuni  34368  omsfval  34379  elcarsg  34390  itgeq12dv  34411  isrrvv  34528  reprinrn  34703  reprdifc  34712  istrkg2d  34751  axtgupdim2ALTV  34753  brafs  34757  bnj956  34860  bnj1146  34875  bnj18eq1  35011  axsepg2  35166  axsepg2ALT  35167  zltp1ne  35226  isacycgr  35261  kur14  35332  pconncn  35340  cnpconn  35346  txpconn  35348  cvmscbv  35374  cvmcov  35379  cvmsi  35381  cvmsval  35382  cvmopnlem  35394  cvmlift2lem10  35428  cvmlift3lem2  35436  cvmlift3lem6  35440  cvmlift3lem7  35441  cvmlift3lem9  35443  cvmlift3  35444  satf0op  35493  sat1el2xp  35495  satffunlem  35517  dmopab3rexdif  35521  mclsssvlem  35678  mclsind  35686  rexxfr3dALT  35755  eldm3  35877  opelco3  35891  dfon2lem6  35902  dfon2lem7  35903  dfon2lem8  35904  dfon2  35906  elfuns  36029  lemsuccf  36055  brofs  36121  5segofs  36122  brifs  36159  ifscgr  36160  brcolinear  36175  lineext  36192  brfs  36195  fscgr  36196  linecgr  36197  btwnconn1lem4  36206  btwnconn1lem8  36210  btwnconn1lem11  36213  btwnconn1lem12  36214  segcon2  36221  brsegle  36224  outsideofeq  36246  funray  36256  funline  36258  fvline  36260  linethru  36269  disjeq12dv  36331  prodeq12sdv  36334  itgeq12sdv  36335  cbvitgvw2  36364  cbvitgdavw  36397  cbvitgdavw2  36413  trer  36432  finminlem  36434  ivthALT  36451  filnetlem4  36497  knoppndvlem21  36648  bj-zfauscl  37041  bj-elgab  37056  bj-imdirvallem  37297  csboprabg  37447  topdifinffinlem  37464  icoreval  37470  isbasisrelowllem1  37472  isbasisrelowllem2  37473  relowlssretop  37480  pibp19  37531  curf  37711  ptrest  37732  poimirlem1  37734  poimirlem13  37746  poimirlem14  37747  poimirlem22  37755  poimirlem24  37757  poimirlem26  37759  poimirlem27  37760  heicant  37768  mblfinlem3  37772  mblfinlem4  37773  mbfresfi  37779  itg2addnclem3  37786  itg2addnc  37787  itg2gt0cn  37788  areacirclem5  37825  cover2  37828  cover2g  37829  fdc  37858  fdc1  37859  heibor1  37923  bfp  37937  rngosn3  38037  drngoi  38064  isdrngo1  38069  isriscg  38097  isfldidl2  38182  eldmxrncnvepres  38531  brressn  38616  islshpat  39189  lcvbr  39193  lshpsmreu  39281  ldual1dim  39338  cvrval  39441  cvrnbtwn3  39448  iscvlat2N  39496  ishlat3N  39526  hlrelat5N  39573  3dim0  39629  llnexatN  39693  islpln5  39707  islvol5  39751  pmapjat1  40025  ltrnu  40293  cdleme02N  40394  cdlemg33b  40879  cdlemg33c  40880  dvhb1dimN  41158  dibelval3  41319  dibopelval3  41320  dib1dim  41337  dibglbN  41338  diblsmopel  41343  dicval  41348  dicopelval  41349  dicelval3  41352  dicelval1sta  41359  dihopelvalcpre  41420  dih1dimatlem  41501  dihpN  41508  dihjatcclem4  41593  lpolsetN  41654  mapdpglem3  41847  hdmapglem7a  42099  sticksstones23  42335  exfinfldd  42369  fimgmcyclem  42703  fimgmcyc  42704  fsuppind  42748  fsuppssindlem2  42750  prjspeclsp  42770  mrefg2  42864  mzpclval  42882  eldiophb  42914  eldioph2lem1  42917  eldioph3  42923  lzenom  42927  diophin  42929  eldiophss  42931  diophrex  42932  eq0rabdioph  42933  pellexlem3  42988  elpell1qr  43004  elpell14qr  43006  elpell1234qr  43008  jm2.27  43165  rmydioph  43171  expdiophlem1  43178  expdioph  43180  pw2f1ocnv  43194  hbtlem1  43280  hbtlem7  43282  dgraalem  43302  dgraaub  43305  dflim7  43430  omabs2  43489  tfsconcatfv2  43497  tfsconcat0i  43502  nadd1suc  43549  ifpbi2  43624  inintabd  43736  cnvcnvintabd  43757  cnvintabd  43760  clcnvlem  43780  iunrelexpmin1  43865  uneqsn  44182  k0004lem2  44305  mnuprdlem1  44429  mnuprdlem2  44430  binomcxplemnotnn0  44513  2sbc6g  44572  2sbc5g  44573  iotasbc  44576  dropab1  44603  dropab2  44604  relpeq5  45105  modelaxreplem3  45137  omssaxinf2  45145  brpermmodel  45160  permaxinf2lem  45169  cbvmpo1  45258  r19.28zf  45319  disjinfi  45352  dmrelrnrel  45386  mullimc  45778  mullimcf  45785  limsuppnfd  45862  limsuppnf  45871  limsupre2  45885  limsupre2mpt  45890  limsupre3  45893  limsupre3mpt  45894  limsupre3uzlem  45895  fourierdlem42  46309  fourierdlem48  46314  fourierdlem50  46316  fourierdlem51  46317  fourierdlem54  46320  fourierdlem86  46352  ovnval2  46705  ovnsubaddlem1  46730  hoiqssbl  46785  vonicclem2  46844  f1cof1b  47239  f1ocof1ob2  47244  funressnbrafv2  47406  dfatdmfcoafv2  47416  2ffzoeq  47489  fundcmpsurbijinj  47572  ichreuopeq  47635  prproropf1olem4  47668  prprspr2  47680  prprsprreu  47681  prprreueq  47682  reuopreuprim  47688  isubgrgrim  48091  grtriprop  48103  isgrtri  48105  opgpgvtx  48217  pgnbgreunbgrlem1  48275  pgnbgreunbgrlem4  48281  grlimedgnedg  48293  rngcsectALTV  48437  rngcinvALTV  48438  ringcsectALTV  48471  ringcinvALTV  48472  lmod1  48654  elbigo2  48714  rrx2vlinest  48903  eloprab1st2nd  49029  i0oii  49081  io1ii  49082  lubeldm2d  49119  glbeldm2d  49120  sectpropdlem  49197  invpropdlem  49199  isopropdlem  49201  uppropd  49342  functhinc  49609  fullthinc  49611