Theorem anbi1d 632

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  633  anbi1  634  pm5.71  1030  cador  1610  drsb1  2500  eleq1w  2820  eleq1d  2822  clelab  2881  rexeqfOLD  3329  rmoeq1OLD  3385  reueq1OLD  3386  rmoeq1f  3391  rabeq  3415  rabeqbidva  3417  rabeqd  3429  rabeqf  3435  cgsex4gOLD  3490  vtocl2gafOLD  3537  vtocl4gaOLD  3544  alexeqg  3607  reu2eqd  3696  sbc2or  3751  sbc5ALT  3771  rexssOLD  4013  psstr  4061  difin2  4255  r19.28z  4457  dfif6  4484  rabsneq  4601  rexreusng  4638  reurexprg  4663  rabsnifsb  4681  ssunsn2  4785  preq12bg  4811  opeq1  4831  eluni  4868  csbuni  4895  unissb  4898  iuneq12d  4978  disjxun  5098  unopab  5180  mpteq12da  5183  mpteq12f  5185  mpteq12dva  5186  dftr2c  5210  axrep1  5227  axreplem  5228  zfrepclf  5238  axsepgfromrep  5241  axsepg  5244  zfauscl  5245  reusv2lem4  5348  rabxfrd  5364  opthg  5433  otthg  5441  copsexgw  5446  copsexg  5447  opeqsng  5459  euotd  5469  elopabw  5482  pocl  5548  xpeq1  5646  elxpi  5654  vtoclr  5695  opbrop  5730  dmopab2rex  5874  resopab2  6003  rnco  6218  dflim2  6383  dffun2  6510  fun11  6574  feq2  6649  f1eq2  6734  f1eq3  6735  foeq2  6751  brprcneu  6832  brprcneuALT  6833  ssimaexg  6928  dmfco  6938  funcnvmpt  6951  fndmdif  6996  respreima  7020  isoeq5  7277  isoini  7294  isopolem  7301  f1oiso  7307  f1oiso2  7308  imaeqsexvOLD  7319  riotaeqdv  7326  oprabidw  7399  oprabid  7400  oprabv  7428  mpoeq123  7440  mpoeq123dva  7442  0mpo0  7451  eloprabga  7477  resoprab  7486  resoprab2  7487  elrnmpores  7506  ov  7512  ov3  7531  ov6g  7532  ovg  7533  imaeqexov  7606  caoftrn  7673  uniuni  7717  limuni3  7804  elxp4  7874  elxp5  7875  opabex3d  7919  opabex3rd  7920  opabex3  7921  releldmdifi  7999  opiota  8013  eloprabi  8017  mptmpoopabbrd  8034  mptmpoopabbrdOLD  8035  cnvf1o  8063  frxp  8078  xporderlem  8079  poxp  8080  fnwelem  8083  poxp2  8095  xpord3pred  8104  poseq  8110  soseq  8111  suppimacnv  8126  rexsupp  8134  mpocurryd  8221  smoel2  8305  omeu  8522  oeeui  8540  omabs  8589  omopth  8600  eldifsucnn  8602  qliftel  8749  brecop  8759  eroveu  8761  erov  8763  ecopovtrn  8769  ixpsnf1o  8888  dom2lem  8941  mapsnend  8985  xpsnen  9001  xpassen  9011  pw2f1olem  9021  xpf1o  9079  unxpdom  9171  domunfican  9234  preleqALT  9538  zfinf  9560  cantnfs  9587  brttrcl  9634  ttrclselem2  9647  tcvalg  9657  r0weon  9934  fseqenlem1  9946  acni2  9968  aceq1  10039  aceq0  10040  dfac5lem4  10048  dfac2a  10052  dfac12lem2  10067  cardcf  10174  cfeq0  10178  cfsuc  10179  cff1  10180  cfss  10187  isf32lem5  10279  fin1a2lem6  10327  zfac  10382  brdom7disj  10453  brdom6disj  10454  axrepnd  10517  axunndlem1  10518  axinfnd  10529  axacndlem5  10534  axacnd  10535  zfcndrep  10537  zfcndinf  10541  zfcndac  10542  pwfseqlem4a  10584  pwfseqlem4  10585  gruina  10741  grothomex  10752  ordpipq  10865  elnpi  10911  genpass  10932  ltprord  10953  reclem2pr  10971  reclem3pr  10972  recexpr  10974  addsrmo  10996  mulsrmo  10997  addsrpr  10998  mulsrpr  10999  ltsosr  11017  mulgt0sr  11028  supsr  11035  ltresr  11063  axpre-lttrn  11089  axpre-mulgt0  11091  prime  12585  peano5uzti  12594  rexuz  12823  ltxr  13041  qbtwnre  13126  xmulneg1  13196  supxr2  13241  ixxval  13281  fzval  13437  preduz  13578  nn0opth2  14207  hashbclem  14387  hashf1lem2  14391  eqwrd  14492  pfxeq  14631  wrd2ind  14658  cshwcsh2id  14763  eqwrds3  14896  cleq1lem  14917  rtrclreclem3  14995  rtrclreclem4  14996  relexpindlem  14998  abslt  15250  absle  15251  lenegsq  15256  abs2difabs  15270  ello12  15451  elo12  15462  o1lo1  15472  rlimuni  15485  lo1resb  15499  o1resb  15501  2clim  15507  rlimcn3  15525  climcn2  15528  addcn2  15529  mulcn2  15531  o1of2  15548  sumeq1  15624  fsum2dlem  15705  modfsummod  15729  prodeq1f  15841  prodeq1  15842  fprod2dlem  15915  nndivdvds  16200  divalg2  16344  smupval  16427  gcdval  16435  gcdass  16486  lcmval  16531  lcmass  16553  rpexp  16661  pythagtriplem2  16757  pythagtrip  16774  vdwapun  16914  0ram  16960  ramub1lem2  16967  pwsle  17425  imasleval  17474  ismre  17521  ismri  17566  iscatd2  17616  dfiso2  17708  isssc  17756  funcpropd  17838  fullpropd  17858  fthres2b  17868  fthres2c  17869  setcsect  18025  cat1lem  18032  cat1  18033  prslem  18232  drsdir  18237  posi  18252  tosso  18352  odudlatb  18460  ipoval  18465  ipolt  18470  dirge  18538  gsumpropd2lem  18616  mgmhmpropd  18635  issgrpv  18658  issgrpn0  18659  ismhm0  18727  mhmpropd  18729  mndind  18765  mgmnsgrpex  18868  issubg3  19086  isga  19232  symgfixelq  19374  psgnfval  19441  psgnval  19448  dprdw  19953  subgdmdprd  19977  isomnd  20064  isrnghm  20389  issubrg  20516  resrhm2b  20547  rngcsect  20581  rngcinv  20582  ringcsect  20615  ringcinv  20616  drngpropd  20714  orngmul  20810  islmod  20827  lmodlema  20828  lmodprop2d  20887  lsslss  20924  lbspropd  21063  lbsacsbs  21123  znleval  21521  islbs4  21799  islinds3  21801  aspval2  21866  psrbag  21885  pf1ind  22311  mdetunilem4  22571  mdetunilem9  22576  istopg  22851  basis2  22907  tg2  22921  iscld  22983  isnei  23059  isneip  23061  neiptoptop  23087  neiptopnei  23088  neitr  23136  restlp  23139  iscn  23191  cnpval  23192  iscnp  23193  regsep  23290  1stcclb  23400  2ndc1stc  23407  2ndcctbss  23411  2ndcdisj  23412  llyi  23430  nllyi  23431  hausmapdom  23456  locfinnei  23479  comppfsc  23488  elkgen  23492  txbas  23523  txcls  23560  txcnpi  23564  ptpjopn  23568  txdis1cn  23591  txtube  23596  txcmplem1  23597  hausdiag  23601  tx1stc  23606  txkgen  23608  xkococn  23616  elqtop  23653  kqreglem1  23697  elmptrab  23783  isfbas  23785  elflim2  23920  elflim  23927  hauspwpwf1  23943  alexsublem  24000  ghmcnp  24071  qustgplem  24077  tsmssubm  24099  elutop  24189  ustuqtop4  24200  isucn  24233  iscfilu  24243  ispsmet  24260  ismet  24279  isxmet  24280  ismet2  24289  imasdsf1olem  24329  blres  24387  elmopn  24398  mopni  24448  neibl  24457  nrmmetd  24530  ngppropd  24593  elcncf  24850  mulc1cncf  24866  elpi1  25013  isclmp  25065  metcld2  25275  pmltpclem1  25417  itg1climres  25683  itg2val  25697  isibl  25734  itgeq1f  25740  itgeq1fOLD  25741  itgeq1  25742  cbvitgv  25746  itgresr  25748  iblcn  25768  itgfsum  25796  dvreslem  25878  dvfsumlem2  26001  dvfsumlem2OLD  26002  deg1ldg  26065  vieta1  26288  ulm2  26362  sincosq2sgn  26476  sincosq4sgn  26478  efopn  26635  dvdsflsumcom  27166  fsumvma2  27193  logfac2  27196  dchrptlem1  27243  lgsdchrval  27333  2lgslem1a  27370  pntibndlem3  27571  pntlemi  27583  pntleme  27587  pnt3  27591  ltsval  27627  nolt02o  27675  leltstr  27741  nocvxminlem  27762  madebday  27908  ltslpss  27916  addsprop  27984  mulsproplemcbv  28123  mulsproplem1  28124  mulsprop  28138  abslts  28257  eucliddivs  28384  bdayfinbndlem2  28476  z12sge0  28491  istrkgld  28543  istrkg2ld  28544  istrkg3ld  28545  axtgsegcon  28548  axtg5seg  28549  axtgpasch  28551  axtgupdim2  28555  legov  28669  islnopp  28823  ishpg  28843  iscgra1  28894  dfcgra2  28914  dfcgrg2  28947  brcgr  28985  brbtwn2  28990  axsegconlem1  29002  axsegcon  29012  axcontlem10  29058  edgssv2  29283  uhgr2edg  29293  isfusgrf1  29405  edgnbusgreu  29452  cplgr3v  29520  vtxdun  29567  upgr2wlk  29752  upgrtrls  29785  upgristrl  29786  upgrf1istrl  29787  dfpth2  29814  2pthnloop  29816  usgr2pth  29849  isclwlke  29862  isclwlkupgr  29863  iswwlksnx  29925  wlknewwlksn  29972  2pthon3v  30028  elwwlks2on  30046  wpthswwlks2on  30049  rusgrnumwwlkl1  30056  rusgrnumwwlkb0  30059  clwwlknp  30124  clwwlkf  30134  erclwwlknsym  30157  erclwwlkntr  30158  clwwlknonwwlknonb  30193  0trl  30209  0spth  30213  0crct  30220  0cycl  30221  upgr4cycl4dv4e  30272  upgriseupth  30294  eupth2lem2  30306  3cyclfrgrrn1  30372  4cycl2vnunb  30377  frgrncvvdeqlem2  30387  frgr2wwlk1  30416  fusgr2wsp2nb  30421  numclwlk1lem1  30456  vciOLD  30649  isvclem  30665  nmoofval  30850  isph  30910  norm3lemt  31240  isch2  31311  cmbr  31672  eigre  31923  eigorth  31926  nmopub  31996  nmfnleub  32013  cvbr  32370  mdbr  32382  dmdbr  32387  chrelat2  32458  mdsymlem2  32492  rexunirn  32578  ifeqeqx  32629  iunrnmptss  32652  fdifsupp  32775  ressupprn  32780  1stpreima  32797  fpwrelmapffslem  32822  archirng  33282  isslmd  33296  slmdlema  33297  urpropd  33325  lindflbs  33472  islbs5  33473  lindfpropd  33475  opprqus0g  33583  idlsrgval  33596  ressply1mon1p  33661  ccfldextdgrr  33850  constrsslem  33919  constrconj  33923  constrlccllem  33931  constrcbvlem  33933  dya2iocuni  34461  omsfval  34472  elcarsg  34483  itgeq12dv  34504  isrrvv  34621  reprinrn  34796  reprdifc  34805  istrkg2d  34844  axtgupdim2ALTV  34846  brafs  34850  bnj956  34953  bnj1146  34967  bnj18eq1  35103  axsepg2  35259  axsepg2ALT  35260  zltp1ne  35326  isacycgr  35361  kur14  35432  pconncn  35440  cnpconn  35446  txpconn  35448  cvmscbv  35474  cvmcov  35479  cvmsi  35481  cvmsval  35482  cvmopnlem  35494  cvmlift2lem10  35528  cvmlift3lem2  35536  cvmlift3lem6  35540  cvmlift3lem7  35541  cvmlift3lem9  35543  cvmlift3  35544  satf0op  35593  sat1el2xp  35595  satffunlem  35617  dmopab3rexdif  35621  mclsssvlem  35778  mclsind  35786  rexxfr3dALT  35855  eldm3  35977  opelco3  35991  dfon2lem6  36002  dfon2lem7  36003  dfon2lem8  36004  dfon2  36006  elfuns  36129  lemsuccf  36155  brofs  36221  5segofs  36222  brifs  36259  ifscgr  36260  brcolinear  36275  lineext  36292  brfs  36295  fscgr  36296  linecgr  36297  btwnconn1lem4  36306  btwnconn1lem8  36310  btwnconn1lem11  36313  btwnconn1lem12  36314  segcon2  36321  brsegle  36324  outsideofeq  36346  funray  36356  funline  36358  fvline  36360  linethru  36369  disjeq12dv  36431  prodeq12sdv  36434  itgeq12sdv  36435  cbvitgvw2  36464  cbvitgdavw  36497  cbvitgdavw2  36513  trer  36532  finminlem  36534  ivthALT  36551  filnetlem4  36597  knoppndvlem21  36754  bj-zfauscl  37172  bj-elgab  37187  bj-imdirvallem  37435  csboprabg  37585  topdifinffinlem  37602  icoreval  37608  isbasisrelowllem1  37610  isbasisrelowllem2  37611  relowlssretop  37618  pibp19  37669  curf  37849  ptrest  37870  poimirlem1  37872  poimirlem13  37884  poimirlem14  37885  poimirlem22  37893  poimirlem24  37895  poimirlem26  37897  poimirlem27  37898  heicant  37906  mblfinlem3  37910  mblfinlem4  37911  mbfresfi  37917  itg2addnclem3  37924  itg2addnc  37925  itg2gt0cn  37926  areacirclem5  37963  cover2  37966  cover2g  37967  fdc  37996  fdc1  37997  heibor1  38061  bfp  38075  rngosn3  38175  drngoi  38202  isdrngo1  38207  isriscg  38235  isfldidl2  38320  raldmqseu  38616  eldmxrncnvepres  38685  brressn  38782  islshpat  39393  lcvbr  39397  lshpsmreu  39485  ldual1dim  39542  cvrval  39645  cvrnbtwn3  39652  iscvlat2N  39700  ishlat3N  39730  hlrelat5N  39777  3dim0  39833  llnexatN  39897  islpln5  39911  islvol5  39955  pmapjat1  40229  ltrnu  40497  cdleme02N  40598  cdlemg33b  41083  cdlemg33c  41084  dvhb1dimN  41362  dibelval3  41523  dibopelval3  41524  dib1dim  41541  dibglbN  41542  diblsmopel  41547  dicval  41552  dicopelval  41553  dicelval3  41556  dicelval1sta  41563  dihopelvalcpre  41624  dih1dimatlem  41705  dihpN  41712  dihjatcclem4  41797  lpolsetN  41858  mapdpglem3  42051  hdmapglem7a  42303  sticksstones23  42539  exfinfldd  42573  fimgmcyclem  42903  fimgmcyc  42904  fsuppind  42948  fsuppssindlem2  42950  prjspeclsp  42970  mrefg2  43064  mzpclval  43082  eldiophb  43114  eldioph2lem1  43117  eldioph3  43123  lzenom  43127  diophin  43129  eldiophss  43131  diophrex  43132  eq0rabdioph  43133  pellexlem3  43188  elpell1qr  43204  elpell14qr  43206  elpell1234qr  43208  jm2.27  43365  rmydioph  43371  expdiophlem1  43378  expdioph  43380  pw2f1ocnv  43394  hbtlem1  43480  hbtlem7  43482  dgraalem  43502  dgraaub  43505  dflim7  43630  omabs2  43689  tfsconcatfv2  43697  tfsconcat0i  43702  nadd1suc  43749  ifpbi2  43823  inintabd  43935  cnvcnvintabd  43956  cnvintabd  43959  clcnvlem  43979  iunrelexpmin1  44064  uneqsn  44381  k0004lem2  44504  mnuprdlem1  44628  mnuprdlem2  44629  binomcxplemnotnn0  44712  2sbc6g  44771  2sbc5g  44772  iotasbc  44775  dropab1  44802  dropab2  44803  relpeq5  45304  modelaxreplem3  45336  omssaxinf2  45344  brpermmodel  45359  permaxinf2lem  45368  cbvmpo1  45457  r19.28zf  45518  disjinfi  45551  dmrelrnrel  45584  mullimc  45976  mullimcf  45983  limsuppnfd  46060  limsuppnf  46069  limsupre2  46083  limsupre2mpt  46088  limsupre3  46091  limsupre3mpt  46092  limsupre3uzlem  46093  fourierdlem42  46507  fourierdlem48  46512  fourierdlem50  46514  fourierdlem51  46515  fourierdlem54  46518  fourierdlem86  46550  ovnval2  46903  ovnsubaddlem1  46928  hoiqssbl  46983  vonicclem2  47042  f1cof1b  47437  f1ocof1ob2  47442  funressnbrafv2  47604  dfatdmfcoafv2  47614  2ffzoeq  47687  fundcmpsurbijinj  47770  ichreuopeq  47833  prproropf1olem4  47866  prprspr2  47878  prprsprreu  47879  prprreueq  47880  reuopreuprim  47886  isubgrgrim  48289  grtriprop  48301  isgrtri  48303  opgpgvtx  48415  pgnbgreunbgrlem1  48473  pgnbgreunbgrlem4  48479  grlimedgnedg  48491  rngcsectALTV  48635  rngcinvALTV  48636  ringcsectALTV  48669  ringcinvALTV  48670  lmod1  48852  elbigo2  48912  rrx2vlinest  49101  eloprab1st2nd  49227  i0oii  49279  io1ii  49280  lubeldm2d  49317  glbeldm2d  49318  sectpropdlem  49395  invpropdlem  49397  isopropdlem  49399  uppropd  49540  functhinc  49807  fullthinc  49809