Theorem anbi1d 642

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 26	. 2 ⊢ (𝜑 → (𝜃 → (𝜓 ↔ 𝜒)))
3	2	pm5.32rd 588	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) ↔ (𝜒 ∧ 𝜃)))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  anbi12d  643  anbi1  644  pm5.71  1043  cador  1635  drsb1  2533  eleq1w  2852  eleq1d  2854  clelab  2913  rmoeq1f  3413  rabeq  3437  rabeqbidva  3439  rabeqd  3451  rabeqf  3457  alexeqg  3619  reu2eqd  3708  sbc2or  3762  sbc5ALT  3782  rexssOLD  4021  psstr  4070  difin2  4262  r19.28z  4468  dfif6  4495  rabsneq  4613  rexreusng  4650  reurexprg  4675  rabsnifsb  4693  ssunsn2  4797  preq12bg  4822  opeq1  4842  eluni  4879  csbuni  4907  unissb  4910  iuneq12d  4990  disjxun  5111  unopab  5195  mpteq12da  5198  mpteq12f  5200  mpteq12dva  5201  dftr2c  5225  axrep1  5243  axreplem  5244  zfrepclf  5256  axsepgfromrep  5259  axsepg  5262  zfauscl  5263  reusv2lem4  5373  rabxfrd  5389  opthg  5460  otthg  5468  copsexgw  5473  copsexgwOLD  5474  copsexg  5475  opeqsng  5487  euotd  5497  elopabw  5511  pocl  5578  xpeq1  5676  elxpi  5684  vtoclr  5725  opbrop  5760  dmopab2rex  5908  resopab2  6039  rnco  6254  dflim2  6420  dffun2  6547  fun11  6611  feq2  6685  f1eq2  6771  f1eq3  6772  foeq2  6790  brprcneu  6872  brprcneuALT  6873  ssimaexg  6968  dmfco  6978  funcnvmpt  6992  fndmdif  7038  respreima  7062  isoeq5  7320  isoini  7337  isopolem  7344  f1oiso  7350  f1oiso2  7351  imaeqsexvOLD  7362  riotaeqdv  7369  oprabidw  7442  oprabid  7443  oprabv  7471  mpoeq123  7483  mpoeq123dva  7485  0mpo0  7494  eloprabga  7520  resoprab  7529  resoprab2  7530  elrnmpores  7549  ov  7555  ov3  7574  ov6g  7575  ovg  7576  imaeqexov  7649  caoftrn  7716  uniuni  7760  limuni3  7847  elxp4  7918  elxp5  7919  opabex3d  7961  opabex3rd  7962  opabex3  7963  releldmdifi  8041  opiota  8055  eloprabi  8059  mptmpoopabbrd  8077  cnvf1o  8105  frxp  8121  xporderlem  8122  poxp  8123  fnwelem  8126  poxp2  8138  xpord3pred  8147  poseq  8153  soseq  8154  suppimacnv  8169  rexsupp  8177  mpocurryd  8264  smoel2  8349  omeu  8569  oeeui  8587  omabs  8636  omopth  8647  eldifsucnn  8649  qliftel  8797  brecop  8807  eroveu  8809  erov  8811  ecopovtrn  8817  ixpsnf1o  8935  dom2lem  8988  mapsnend  9032  xpsnen  9048  xpassen  9058  pw2f1olem  9068  xpf1o  9126  unxpdom  9218  domunfican  9280  preleqALT  9585  zfinf  9607  cantnfs  9634  brttrcl  9681  ttrclselem2  9694  tcvalg  9704  r0weon  9995  fseqenlem1  10007  acni2  10029  aceq1  10100  aceq0  10101  dfac5lem4  10109  dfac2a  10112  dfac12lem2  10127  cardcf  10234  cfeq0  10239  cfsuc  10240  cff1  10241  cfss  10248  isf32lem5  10340  fin1a2lem6  10388  zfac  10443  brdom7disj  10514  brdom6disj  10515  axrepnd  10578  axunndlem1  10579  axinfnd  10590  axacndlem5  10595  axacnd  10596  zfcndrep  10598  zfcndinf  10602  zfcndac  10603  pwfseqlem4a  10645  pwfseqlem4  10646  gruina  10802  grothomex  10813  ordpipq  10926  elnpi  10972  genpass  10993  ltprord  11014  reclem2pr  11032  reclem3pr  11033  recexpr  11035  addsrmo  11057  mulsrmo  11058  addsrpr  11059  mulsrpr  11060  ltsosr  11078  mulgt0sr  11089  supsr  11096  ltresr  11124  axpre-lttrn  11150  axpre-mulgt0  11152  prime  12676  peano5uzti  12685  rexuz  12921  ltxr  13139  qbtwnre  13224  xmulneg1  13294  supxr2  13339  ixxval  13379  fzval  13536  preduz  13677  nn0opth2  14307  hashbclem  14488  hashf1lem2  14492  eqwrd  14593  pfxeq  14732  wrd2ind  14759  cshwcsh2id  14864  eqwrds3  14997  cleq1lem  15018  rtrclreclem3  15096  rtrclreclem4  15097  relexpindlem  15099  abslt  15365  absle  15366  lenegsq  15371  abs2difabs  15385  ello12  15566  elo12  15577  o1lo1  15587  rlimuni  15600  lo1resb  15614  o1resb  15616  2clim  15622  rlimcn3  15640  climcn2  15643  addcn2  15644  mulcn2  15646  o1of2  15663  sumeq1  15739  fsum2dlem  15820  modfsummod  15845  prodeq1f  15959  prodeq1  15960  fprod2dlem  16033  nndivdvds  16318  divalg2  16462  smupval  16545  gcdval  16553  gcdass  16604  lcmval  16649  lcmass  16671  rpexp  16780  pythagtriplem2  16876  pythagtrip  16893  vdwapun  17033  0ram  17079  ramub1lem2  17086  pwsle  17545  imasleval  17594  ismre  17641  ismri  17686  iscatd2  17736  dfiso2  17828  isssc  17876  funcpropd  17958  fullpropd  17978  fthres2b  17988  fthres2c  17989  setcsect  18145  cat1lem  18152  cat1  18153  prslem  18352  drsdir  18357  posi  18372  tosso  18472  odudlatb  18580  ipoval  18585  ipolt  18590  dirge  18658  gsumpropd2lem  18736  mgmhmpropd  18755  issgrpv  18778  issgrpn0  18779  ismhm0  18847  mhmpropd  18849  mndind  18886  mgmnsgrpex  18992  issubg3  19210  isga  19360  symgfixelq  19502  psgnfval  19569  psgnval  19576  dprdw  20081  subgdmdprd  20105  isomnd  20192  isrnghm  20522  issubrg  20655  resrhm2b  20686  rngcsect  20720  rngcinv  20721  ringcsect  20754  ringcinv  20755  drngpropd  20850  orngmul  20945  islmod  20962  lmodlema  20963  lmodprop2d  21022  lsslss  21059  lbspropd  21197  lbsacsbs  21257  znleval  21672  islbs4  21950  islinds3  21952  aspval2  22016  psrbag  22035  pf1ind  22483  mdetunilem4  22740  mdetunilem9  22745  istopg  23020  basis2  23076  tg2  23090  iscld  23152  isnei  23228  isneip  23230  neiptoptop  23256  neiptopnei  23257  neitr  23305  restlp  23308  iscn  23360  cnpval  23361  iscnp  23362  regsep  23459  1stcclb  23569  2ndc1stc  23576  2ndcctbss  23580  2ndcdisj  23581  llyi  23599  nllyi  23600  hausmapdom  23625  locfinnei  23648  comppfsc  23657  elkgen  23661  txbas  23692  txcls  23729  txcnpi  23733  ptpjopn  23737  txdis1cn  23760  txtube  23765  txcmplem1  23766  hausdiag  23770  tx1stc  23775  txkgen  23777  xkococn  23785  elqtop  23822  kqreglem1  23866  elmptrab  23952  isfbas  23954  elflim2  24089  elflim  24096  hauspwpwf1  24112  alexsublem  24169  ghmcnp  24240  qustgplem  24246  tsmssubm  24268  elutop  24358  ustuqtop4  24369  isucn  24402  iscfilu  24412  ispsmet  24429  ismet  24448  isxmet  24449  ismet2  24458  imasdsf1olem  24498  blres  24556  elmopn  24567  mopni  24617  neibl  24626  nrmmetd  24699  ngppropd  24762  elcncf  25016  mulc1cncf  25032  elpi1  25172  isclmp  25224  metcld2  25434  pmltpclem1  25575  itg1climres  25841  itg2val  25855  isibl  25892  itgeq1f  25898  itgeq1fOLD  25899  itgeq1  25900  cbvitgv  25904  itgresr  25906  iblcn  25926  itgfsum  25954  dvreslem  26036  dvfsumlem2  26154  deg1ldg  26217  vieta1  26441  ulm2  26513  sincosq2sgn  26629  sincosq4sgn  26631  efopn  26788  dvdsflsumcom  27317  fsumvma2  27343  logfac2  27346  dchrptlem1  27393  lgsdchrval  27483  2lgslem1a  27520  pntibndlem3  27721  pntlemi  27733  pntleme  27737  pnt3  27741  ltsval  27776  nolt02o  27824  leltstr  27890  nocvxminlem  27912  madebday  28058  ltslpss  28066  addsprop  28134  mulsproplemcbv  28273  mulsproplem1  28274  mulsprop  28288  abslts  28407  eucliddivs  28534  bdayfinbndlem2  28626  z12sge0  28641  istrkgld  28693  istrkg2ld  28694  istrkg3ld  28695  axtgsegcon  28698  axtg5seg  28699  axtgpasch  28701  axtgupdim2  28705  legov  28819  islnopp  28978  ishpg  28999  iscgra1  29077  dfcgra2  29097  dfcgrg2  29134  brprlng  29142  brcgr  29190  brbtwn2  29195  axsegconlem1  29207  axsegcon  29217  axcontlem10  29263  edgssv2  29488  uhgr2edg  29498  isfusgrf1  29610  edgnbusgreu  29657  cplgr3v  29725  vtxdun  29771  upgr2wlk  29956  upgrtrls  29989  upgristrl  29990  upgrf1istrl  29991  dfpth2  30018  2pthnloop  30020  usgr2pth  30053  isclwlke  30066  isclwlkupgr  30067  iswwlksnx  30129  wlknewwlksn  30176  2pthon3v  30232  elwwlks2on  30250  wpthswwlks2on  30253  rusgrnumwwlkl1  30260  rusgrnumwwlkb0  30263  clwwlknp  30328  clwwlkf  30338  erclwwlknsym  30361  erclwwlkntr  30362  clwwlknonwwlknonb  30397  0trl  30413  0spth  30417  0crct  30424  0cycl  30425  upgr4cycl4dv4e  30476  upgriseupth  30498  eupth2lem2  30510  3cyclfrgrrn1  30576  4cycl2vnunb  30581  frgrncvvdeqlem2  30591  frgr2wwlk1  30620  fusgr2wsp2nb  30625  numclwlk1lem1  30660  vciOLD  30853  isvclem  30869  nmoofval  31054  isph  31114  norm3lemt  31444  isch2  31515  cmbr  31876  eigre  32127  eigorth  32130  nmopub  32200  nmfnleub  32217  cvbr  32574  mdbr  32586  dmdbr  32591  chrelat2  32662  mdsymlem2  32696  rexunirn  32778  ifeqeqx  32828  iunrnmptss  32850  fdifsupp  32970  ressupprn  32975  1stpreima  32992  fpwrelmapffslem  33017  archirng  33448  isslmd  33462  slmdlema  33463  urpropd  33490  lindflbs  33635  islbs5  33636  lindfpropd  33638  opprqus0g  33716  idlsrgval  33737  ressply1mon1p  33802  ccfldextdgrr  34006  constrsslem  34075  constrconj  34079  constrlccllem  34087  constrcbvlem  34089  dya2iocuni  34617  omsfval  34628  elcarsg  34639  itgeq12dv  34660  isrrvv  34777  reprinrn  34949  reprdifc  34958  istrkg2d  34997  axtgupdim2ALTV  34999  brafs  35006  bnj956  35109  bnj1146  35123  bnj18eq1  35259  axsepg2  35475  axsepg3  35476  axsepg3ALT  35477  axsepg4  35478  axsepg5  35479  zltp1ne  35499  isacycgr  35535  kur14  35606  pconncn  35614  cnpconn  35620  txpconn  35622  cvmscbv  35648  cvmcov  35653  cvmsi  35655  cvmsval  35656  cvmopnlem  35668  cvmlift2lem10  35702  cvmlift3lem2  35710  cvmlift3lem6  35714  cvmlift3lem7  35715  cvmlift3lem9  35717  cvmlift3  35718  satf0op  35767  sat1el2xp  35769  satffunlem  35791  dmopab3rexdif  35795  mclsssvlem  35952  mclsind  35960  rexxfr3dALT  36029  eldm3  36151  opelco3  36165  dfon2lem6  36176  dfon2lem7  36177  dfon2lem8  36178  dfon2  36180  elfuns  36303  lemsuccf  36329  brofs  36395  5segofs  36396  brifs  36433  ifscgr  36434  brcolinear  36449  lineext  36466  brfs  36469  fscgr  36470  linecgr  36471  btwnconn1lem4  36480  btwnconn1lem8  36484  btwnconn1lem11  36487  btwnconn1lem12  36488  segcon2  36495  brsegle  36498  outsideofeq  36520  funray  36530  funline  36532  fvline  36534  linethru  36543  disjeq12dv  36615  prodeq12sdv  36618  itgeq12sdv  36619  cbvitgvw2  36648  cbvitgdavw  36681  cbvitgdavw2  36697  trer  36715  finminlem  36717  ivthALT  36734  filnetlem4  36780  axtco1  36872  axtco1from2  36874  ttcexg  36931  mh-infprim1bi  36945  knoppndvlem21  37009  bj-zfauscl  37447  bj-elgab  37462  bj-imdirvallem  37711  csboprabg  37863  topdifinffinlem  37880  icoreval  37886  isbasisrelowllem1  37888  isbasisrelowllem2  37889  relowlssretop  37896  pibp19  37947  curf  38136  ptrest  38157  poimirlem1  38159  poimirlem13  38171  poimirlem14  38172  poimirlem22  38180  poimirlem24  38182  poimirlem26  38184  poimirlem27  38185  heicant  38193  mblfinlem3  38197  mblfinlem4  38198  mbfresfi  38204  itg2addnclem3  38211  itg2addnc  38212  itg2gt0cn  38213  areacirclem5  38250  cover2  38253  cover2g  38254  fdc  38283  fdc1  38284  heibor1  38348  bfp  38362  rngosn3  38462  drngoi  38489  isdrngo1  38494  isriscg  38522  isfldidl2  38607  raldmqseu  38903  eldmxrncnvepres  38972  brressn  39069  islshpat  39680  lcvbr  39684  lshpsmreu  39772  ldual1dim  39829  cvrval  39932  cvrnbtwn3  39939  iscvlat2N  39987  ishlat3N  40017  hlrelat5N  40064  3dim0  40120  llnexatN  40184  islpln5  40198  islvol5  40242  pmapjat1  40516  ltrnu  40784  cdleme02N  40885  cdlemg33b  41370  cdlemg33c  41371  dvhb1dimN  41649  dibelval3  41810  dibopelval3  41811  dib1dim  41828  dibglbN  41829  diblsmopel  41834  dicval  41839  dicopelval  41840  dicelval3  41843  dicelval1sta  41850  dihopelvalcpre  41911  dih1dimatlem  41992  dihpN  41999  dihjatcclem4  42084  lpolsetN  42145  mapdpglem3  42338  hdmapglem7a  42590  sticksstones23  42825  exfinfldd  42859  fimgmcyclem  43192  fimgmcyc  43193  fsuppind  43213  fsuppssindlem2  43215  prjspeclsp  43235  mrefg2  43329  mzpclval  43347  eldiophb  43379  eldioph2lem1  43382  eldioph3  43388  lzenom  43392  diophin  43394  eldiophss  43396  diophrex  43397  eq0rabdioph  43398  pellexlem3  43449  elpell1qr  43465  elpell14qr  43467  elpell1234qr  43469  jm2.27  43626  rmydioph  43632  expdiophlem1  43639  expdioph  43641  pw2f1ocnv  43655  hbtlem1  43741  hbtlem7  43743  dgraalem  43763  dgraaub  43766  dflim7  43891  omabs2  43950  tfsconcatfv2  43958  tfsconcat0i  43963  nadd1suc  44010  ifpbi2  44084  inintabd  44196  cnvcnvintabd  44217  cnvintabd  44220  clcnvlem  44240  iunrelexpmin1  44325  uneqsn  44642  k0004lem2  44765  mnuprdlem1  44873  mnuprdlem2  44874  binomcxplemnotnn0  44957  2sbc6g  45016  2sbc5g  45017  iotasbc  45020  dropab1  45047  dropab2  45048  relpeq5  45548  modelaxreplem3  45580  omssaxinf2  45588  brpermmodel  45603  permaxinf2lem  45612  cbvmpo1  45707  r19.28zf  45768  disjinfi  45801  dmrelrnrel  45833  mullimc  46223  mullimcf  46230  limsuppnfd  46307  limsuppnf  46316  limsupre2  46330  limsupre2mpt  46335  limsupre3  46338  limsupre3mpt  46339  limsupre3uzlem  46340  fourierdlem42  46754  fourierdlem48  46759  fourierdlem50  46761  fourierdlem51  46762  fourierdlem54  46765  fourierdlem86  46797  ovnval2  47150  ovnsubaddlem1  47175  hoiqssbl  47230  vonicclem2  47289  f1cof1b  47702  f1ocof1ob2  47707  funressnbrafv2  47869  dfatdmfcoafv2  47879  2ffzoeq  47953  fundcmpsurbijinj  48047  ichreuopeq  48110  prproropf1olem4  48143  prprspr2  48155  prprsprreu  48156  prprreueq  48157  reuopreuprim  48163  nprmmul3  48166  isubgrgrim  48582  grtriprop  48594  isgrtri  48596  opgpgvtx  48708  pgnbgreunbgrlem1  48766  pgnbgreunbgrlem4  48772  grlimedgnedg  48784  rngcsectALTV  48928  rngcinvALTV  48929  ringcsectALTV  48962  ringcinvALTV  48963  lmod1  49156  elbigo2  49216  rrx2vlinest  49405  eloprab1st2nd  49530  i0oii  49582  io1ii  49583  lubeldm2d  49620  glbeldm2d  49621  sectpropdlem  49698  invpropdlem  49700  isopropdlem  49702  uppropd  49843  functhinc  50110  fullthinc  50112