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 579	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) ↔ (𝜒 ∧ 𝜃)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  anbi12d  632  anbi1  633  pm5.71  1027  cador  1610  drsb1  2495  eleq1w  2817  eleq1d  2819  clelab  2880  rexeqfOLD  3352  rmoeq1OLD  3417  reueq1OLD  3418  rmoeq1f  3421  rabeq  3447  rabeqd  3461  rabeqf  3467  rabeqiOLD  3472  cgsex4gOLD  3522  vtocl2gaf  3568  vtocl4ga  3573  alexeqg  3640  elrabiOLD  3679  reu2eqd  3733  sbc2or  3787  sbc5ALT  3807  rexss  4056  psstr  4105  difin2  4292  r19.28z  4498  dfif6  4532  rexreusng  4684  reurexprg  4709  rabsnifsb  4727  ssunsn2  4831  preq12bg  4855  opeq1  4874  eluni  4912  csbuni  4941  unissb  4944  disjxun  5147  unopab  5231  mpteq12da  5234  mpteq12f  5237  mpteq12dva  5238  dftr2c  5269  axrep1  5287  axreplem  5288  zfrepclf  5295  axsepgfromrep  5298  axsepg  5301  zfauscl  5302  reusv2lem4  5400  rabxfrd  5416  opthg  5478  otthg  5486  copsexgw  5491  copsexg  5492  opeqsng  5504  euotd  5514  elopabw  5527  pocl  5596  poclOLD  5597  xpeq1  5691  elxpi  5699  vtoclr  5740  opbrop  5774  dmopab2rex  5918  resopab2  6037  dflim2  6422  dffun2  6554  fun11  6623  feq2  6700  f1eq2  6784  f1eq3  6785  foeq2  6803  brprcneu  6882  brprcneuALT  6883  ssimaexg  6978  dmfco  6988  fndmdif  7044  respreima  7068  isoeq5  7318  isoini  7335  isopolem  7342  f1oiso  7348  f1oiso2  7349  imaeqsexv  7360  riotaeqdv  7366  oprabidw  7440  oprabid  7441  oprabv  7469  mpoeq123  7481  mpoeq123dva  7483  0mpo0  7492  eloprabga  7516  eloprabgaOLD  7517  resoprab  7526  resoprab2  7527  elrnmpores  7546  ov  7552  ov3  7570  ov6g  7571  ovg  7572  imaeqexov  7645  caoftrn  7708  uniuni  7749  limuni3  7841  elxp4  7913  elxp5  7914  opabex3d  7952  opabex3rd  7953  opabex3  7954  releldmdifi  8031  opiota  8045  eloprabi  8049  mptmpoopabbrd  8067  mptmpoopabbrdOLD  8069  cnvf1o  8097  frxp  8112  xporderlem  8113  poxp  8114  fnwelem  8117  poxp2  8129  xpord3pred  8138  poseq  8144  soseq  8145  suppimacnv  8159  rexsupp  8167  mpocurryd  8254  smoel2  8363  omeu  8585  oeeui  8602  omabs  8650  omopth  8661  eldifsucnn  8663  qliftel  8794  brecop  8804  eroveu  8806  erov  8808  ecopovtrn  8814  ixpsnf1o  8932  dom2lem  8988  mapsnend  9036  xpsnen  9055  xpassen  9066  pw2f1olem  9076  xpf1o  9139  unxpdom  9253  domunfican  9320  preleqALT  9612  zfinf  9634  cantnfs  9661  brttrcl  9708  ttrclselem2  9721  tcvalg  9733  r0weon  10007  fseqenlem1  10019  acni2  10041  aceq1  10112  aceq0  10113  dfac2a  10124  dfac12lem2  10139  cardcf  10247  cfeq0  10251  cfsuc  10252  cff1  10253  cfss  10260  isf32lem5  10352  fin1a2lem6  10400  zfac  10455  brdom7disj  10526  brdom6disj  10527  axrepnd  10589  axunndlem1  10590  axinfnd  10601  axacndlem5  10606  axacnd  10607  zfcndrep  10609  zfcndinf  10613  zfcndac  10614  pwfseqlem4a  10656  pwfseqlem4  10657  gruina  10813  grothomex  10824  ordpipq  10937  elnpi  10983  genpass  11004  ltprord  11025  reclem2pr  11043  reclem3pr  11044  recexpr  11046  addsrmo  11068  mulsrmo  11069  addsrpr  11070  mulsrpr  11071  ltsosr  11089  mulgt0sr  11100  supsr  11107  ltresr  11135  axpre-lttrn  11161  axpre-mulgt0  11163  prime  12643  peano5uzti  12652  rexuz  12882  ltxr  13095  qbtwnre  13178  xmulneg1  13248  supxr2  13293  ixxval  13332  fzval  13486  preduz  13623  nn0opth2  14232  hashbclem  14411  hashf1lem2  14417  eqwrd  14507  pfxeq  14646  wrd2ind  14673  cshwcsh2id  14779  eqwrds3  14912  cleq1lem  14929  rtrclreclem3  15007  rtrclreclem4  15008  relexpindlem  15010  abslt  15261  absle  15262  lenegsq  15267  abs2difabs  15281  ello12  15460  elo12  15471  o1lo1  15481  rlimuni  15494  lo1resb  15508  o1resb  15510  2clim  15516  rlimcn3  15534  climcn2  15537  addcn2  15538  mulcn2  15540  o1of2  15557  sumeq1  15635  fsum2dlem  15716  modfsummod  15740  prodeq1f  15852  fprod2dlem  15924  nndivdvds  16206  divalg2  16348  smupval  16429  gcdval  16437  gcdass  16489  lcmval  16529  lcmass  16551  rpexp  16659  pythagtriplem2  16750  pythagtrip  16767  vdwapun  16907  0ram  16953  ramub1lem2  16960  pwsle  17438  imasleval  17487  ismre  17534  ismri  17575  iscatd2  17625  dfiso2  17719  isssc  17767  funcpropd  17851  fullpropd  17871  fthres2b  17881  fthres2c  17882  setcsect  18039  cat1lem  18046  cat1  18047  prslem  18251  drsdir  18255  posi  18270  tosso  18372  odudlatb  18478  ipoval  18483  ipolt  18488  dirge  18556  gsumpropd2lem  18598  issgrpv  18612  issgrpn0  18613  mhmpropd  18678  mndind  18709  mgmnsgrpex  18812  issubg3  19024  isga  19155  symgfixelq  19301  psgnfval  19368  psgnval  19375  dprdw  19880  subgdmdprd  19904  issubrg  20319  resrhm2b  20349  drngpropd  20394  islmod  20475  lmodlema  20476  lmodprop2d  20534  lsslss  20572  lbspropd  20710  lbsacsbs  20769  znleval  21110  islbs4  21387  islinds3  21389  aspval2  21452  psrbag  21470  pf1ind  21874  mdetunilem4  22117  mdetunilem9  22122  istopg  22397  basis2  22454  tg2  22468  iscld  22531  isnei  22607  isneip  22609  neiptoptop  22635  neiptopnei  22636  neitr  22684  restlp  22687  iscn  22739  cnpval  22740  iscnp  22741  regsep  22838  1stcclb  22948  2ndc1stc  22955  2ndcctbss  22959  2ndcdisj  22960  llyi  22978  nllyi  22979  hausmapdom  23004  locfinnei  23027  comppfsc  23036  elkgen  23040  txbas  23071  txcls  23108  txcnpi  23112  ptpjopn  23116  txdis1cn  23139  txtube  23144  txcmplem1  23145  hausdiag  23149  tx1stc  23154  txkgen  23156  xkococn  23164  elqtop  23201  kqreglem1  23245  elmptrab  23331  isfbas  23333  elflim2  23468  elflim  23475  hauspwpwf1  23491  alexsublem  23548  ghmcnp  23619  qustgplem  23625  tsmssubm  23647  elutop  23738  ustuqtop4  23749  isucn  23783  iscfilu  23793  ispsmet  23810  ismet  23829  isxmet  23830  ismet2  23839  imasdsf1olem  23879  blres  23937  elmopn  23948  mopni  24001  neibl  24010  nrmmetd  24083  ngppropd  24146  elcncf  24405  mulc1cncf  24421  elpi1  24561  isclmp  24613  metcld2  24824  pmltpclem1  24965  itg1climres  25232  itg2val  25246  isibl  25283  itgeq1f  25289  itgresr  25296  iblcn  25316  itgfsum  25344  dvreslem  25426  dvfsumlem2  25544  deg1ldg  25610  vieta1  25825  ulm2  25897  sincosq2sgn  26009  sincosq4sgn  26011  efopn  26166  dvdsflsumcom  26692  fsumvma2  26717  logfac2  26720  dchrptlem1  26767  lgsdchrval  26857  2lgslem1a  26894  pntibndlem3  27095  pntlemi  27107  pntleme  27111  pnt3  27115  sltval  27150  nolt02o  27198  slelttr  27260  nocvxminlem  27279  madebday  27395  sltlpss  27402  addsprop  27462  mulsproplemcbv  27574  mulsproplem1  27575  mulsprop  27589  istrkgld  27741  istrkg2ld  27742  istrkg3ld  27743  axtgsegcon  27746  axtg5seg  27747  axtgpasch  27749  axtgupdim2  27753  legov  27867  islnopp  28021  ishpg  28041  iscgra1  28092  dfcgra2  28112  dfcgrg2  28145  brcgr  28189  brbtwn2  28194  axsegconlem1  28206  axsegcon  28216  axcontlem10  28262  edgssv2  28486  uhgr2edg  28496  isfusgrf1  28608  edgnbusgreu  28655  cplgr3v  28723  vtxdun  28769  upgr2wlk  28956  upgrtrls  28989  upgristrl  28990  upgrf1istrl  28991  2pthnloop  29019  usgr2pth  29052  isclwlke  29065  isclwlkupgr  29066  iswwlksnx  29125  wlknewwlksn  29172  2pthon3v  29228  elwwlks2on  29244  wpthswwlks2on  29246  rusgrnumwwlkl1  29253  rusgrnumwwlkb0  29256  clwwlknp  29321  clwwlkf  29331  erclwwlknsym  29354  erclwwlkntr  29355  clwwlknonwwlknonb  29390  0trl  29406  0spth  29410  0crct  29417  0cycl  29418  upgr4cycl4dv4e  29469  upgriseupth  29491  eupth2lem2  29503  3cyclfrgrrn1  29569  4cycl2vnunb  29574  frgrncvvdeqlem2  29584  frgr2wwlk1  29613  fusgr2wsp2nb  29618  numclwlk1lem1  29653  vciOLD  29845  isvclem  29861  nmoofval  30046  isph  30106  norm3lemt  30436  isch2  30507  cmbr  30868  eigre  31119  eigorth  31122  nmopub  31192  nmfnleub  31209  cvbr  31566  mdbr  31578  dmdbr  31583  chrelat2  31654  mdsymlem2  31688  rexunirn  31763  ifeqeqx  31805  iunrnmptss  31828  funcnvmpt  31923  ressupprn  31943  1stpreima  31959  fpwrelmapffslem  31988  isomnd  32250  archirng  32365  isslmd  32378  slmdlema  32379  urpropd  32409  orngmul  32452  lindflbs  32526  islbs5  32527  lindfpropd  32529  opprqus0g  32635  idlsrgval  32648  ressply1mon1p  32688  ccfldextdgrr  32777  dya2iocuni  33313  omsfval  33324  elcarsg  33335  itgeq12dv  33356  isrrvv  33473  reprinrn  33661  reprdifc  33670  istrkg2d  33709  axtgupdim2ALTV  33711  brafs  33715  bnj956  33818  bnj1146  33833  bnj18eq1  33969  zltp1ne  34130  isacycgr  34167  kur14  34238  pconncn  34246  cnpconn  34252  txpconn  34254  cvmscbv  34280  cvmcov  34285  cvmsi  34287  cvmsval  34288  cvmopnlem  34300  cvmlift2lem10  34334  cvmlift3lem2  34342  cvmlift3lem6  34346  cvmlift3lem7  34347  cvmlift3lem9  34349  cvmlift3  34350  satf0op  34399  sat1el2xp  34401  satffunlem  34423  dmopab3rexdif  34427  mclsssvlem  34584  mclsind  34592  eldm3  34762  opelco3  34777  dfon2lem6  34791  dfon2lem7  34792  dfon2lem8  34793  dfon2  34795  elfuns  34918  brsuccf  34944  brofs  35008  5segofs  35009  brifs  35046  ifscgr  35047  brcolinear  35062  lineext  35079  brfs  35082  fscgr  35083  linecgr  35084  btwnconn1lem4  35093  btwnconn1lem8  35097  btwnconn1lem11  35100  btwnconn1lem12  35101  segcon2  35108  brsegle  35111  outsideofeq  35133  funray  35143  funline  35145  fvline  35147  linethru  35156  gg-dvfsumlem2  35214  trer  35249  finminlem  35251  ivthALT  35268  filnetlem4  35314  knoppndvlem21  35456  bj-zfauscl  35852  bj-elgab  35867  bj-imdirvallem  36109  csboprabg  36259  topdifinffinlem  36276  icoreval  36282  isbasisrelowllem1  36284  isbasisrelowllem2  36285  relowlssretop  36292  pibp19  36343  wl-ax11-lem8  36502  curf  36514  ptrest  36535  poimirlem1  36537  poimirlem13  36549  poimirlem14  36550  poimirlem22  36558  poimirlem24  36560  poimirlem26  36562  poimirlem27  36563  heicant  36571  mblfinlem3  36575  mblfinlem4  36576  mbfresfi  36582  itg2addnclem3  36589  itg2addnc  36590  itg2gt0cn  36591  areacirclem5  36628  cover2  36631  cover2g  36632  fdc  36661  fdc1  36662  heibor1  36726  bfp  36740  rngosn3  36840  drngoi  36867  isdrngo1  36872  isriscg  36900  isfldidl2  36985  brressn  37359  islshpat  37935  lcvbr  37939  lshpsmreu  38027  ldual1dim  38084  cvrval  38187  cvrnbtwn3  38194  iscvlat2N  38242  ishlat3N  38272  hlrelat5N  38320  3dim0  38376  llnexatN  38440  islpln5  38454  islvol5  38498  pmapjat1  38772  ltrnu  39040  cdleme02N  39141  cdlemg33b  39626  cdlemg33c  39627  dvhb1dimN  39905  dibelval3  40066  dibopelval3  40067  dib1dim  40084  dibglbN  40085  diblsmopel  40090  dicval  40095  dicopelval  40096  dicelval3  40099  dicelval1sta  40106  dihopelvalcpre  40167  dih1dimatlem  40248  dihpN  40255  dihjatcclem4  40340  lpolsetN  40401  mapdpglem3  40594  hdmapglem7a  40846  fsuppind  41210  fsuppssindlem2  41212  prjspeclsp  41402  mrefg2  41493  mzpclval  41511  eldiophb  41543  eldioph2lem1  41546  eldioph3  41552  lzenom  41556  diophin  41558  eldiophss  41560  diophrex  41561  eq0rabdioph  41562  pellexlem3  41617  elpell1qr  41633  elpell14qr  41635  elpell1234qr  41637  jm2.27  41795  rmydioph  41801  expdiophlem1  41808  expdioph  41810  pw2f1ocnv  41824  hbtlem1  41913  hbtlem7  41915  dgraalem  41935  dgraaub  41938  dflim7  42071  omabs2  42130  tfsconcatfv2  42138  tfsconcat0i  42143  nadd1suc  42190  ifpbi2  42266  inintabd  42378  cnvcnvintabd  42399  cnvintabd  42402  clcnvlem  42422  iunrelexpmin1  42507  uneqsn  42824  k0004lem2  42947  mnuprdlem1  43079  mnuprdlem2  43080  binomcxplemnotnn0  43163  2sbc6g  43222  2sbc5g  43223  iotasbc  43226  dropab1  43254  dropab2  43255  cbvmpo1  43835  r19.28zf  43901  disjinfi  43939  dmrelrnrel  43973  mullimc  44380  mullimcf  44387  limsuppnfd  44466  limsuppnf  44475  limsupre2  44489  limsupre2mpt  44494  limsupre3  44497  limsupre3mpt  44498  limsupre3uzlem  44499  fourierdlem42  44913  fourierdlem48  44918  fourierdlem50  44920  fourierdlem51  44921  fourierdlem54  44924  fourierdlem86  44956  ovnval2  45309  ovnsubaddlem1  45334  hoiqssbl  45389  vonicclem2  45448  f1cof1b  45833  f1ocof1ob2  45838  funressnbrafv2  46000  dfatdmfcoafv2  46010  2ffzoeq  46084  fundcmpsurbijinj  46126  ichreuopeq  46189  prproropf1olem4  46222  prprspr2  46234  prprsprreu  46235  prprreueq  46236  reuopreuprim  46242  mgmhmpropd  46603  ismhm0  46623  isrnghm  46738  rngcsect  46926  rngcinv  46927  rngcsectALTV  46938  rngcinvALTV  46939  ringcsect  46977  ringcinv  46978  ringcsectALTV  47001  ringcinvALTV  47002  lmod1  47221  elbigo2  47286  rrx2vlinest  47475  i0oii  47600  io1ii  47601  lubeldm2d  47639  glbeldm2d  47640  functhinc  47713  fullthinc  47714