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  rmoeq1f  3380  rabeq  3404  rabeqbidva  3406  rabeqd  3418  rabeqf  3424  vtocl2gafOLD  3524  vtocl4gaOLD  3531  alexeqg  3594  reu2eqd  3683  sbc2or  3738  sbc5ALT  3758  rexssOLD  4000  psstr  4048  difin2  4242  r19.28z  4443  dfif6  4470  rabsneq  4587  rexreusng  4624  reurexprg  4649  rabsnifsb  4667  ssunsn2  4771  preq12bg  4797  opeq1  4817  eluni  4854  csbuni  4881  unissb  4884  iuneq12d  4964  disjxun  5084  unopab  5166  mpteq12da  5169  mpteq12f  5171  mpteq12dva  5172  dftr2c  5196  axrep1  5214  axreplem  5215  zfrepclf  5227  axsepgfromrep  5230  axsepg  5233  zfauscl  5234  reusv2lem4  5339  rabxfrd  5355  opthg  5426  otthg  5434  copsexgw  5439  copsexg  5440  opeqsng  5452  euotd  5462  elopabw  5475  pocl  5541  xpeq1  5639  elxpi  5647  vtoclr  5688  opbrop  5723  dmopab2rex  5867  resopab2  5996  rnco  6211  dflim2  6376  dffun2  6503  fun11  6567  feq2  6642  f1eq2  6727  f1eq3  6728  foeq2  6744  brprcneu  6825  brprcneuALT  6826  ssimaexg  6921  dmfco  6931  funcnvmpt  6944  fndmdif  6989  respreima  7013  isoeq5  7270  isoini  7287  isopolem  7294  f1oiso  7300  f1oiso2  7301  imaeqsexvOLD  7312  riotaeqdv  7319  oprabidw  7392  oprabid  7393  oprabv  7421  mpoeq123  7433  mpoeq123dva  7435  0mpo0  7444  eloprabga  7470  resoprab  7479  resoprab2  7480  elrnmpores  7499  ov  7505  ov3  7524  ov6g  7525  ovg  7526  imaeqexov  7599  caoftrn  7666  uniuni  7710  limuni3  7797  elxp4  7867  elxp5  7868  opabex3d  7912  opabex3rd  7913  opabex3  7914  releldmdifi  7992  opiota  8006  eloprabi  8010  mptmpoopabbrd  8027  cnvf1o  8055  frxp  8070  xporderlem  8071  poxp  8072  fnwelem  8075  poxp2  8087  xpord3pred  8096  poseq  8102  soseq  8103  suppimacnv  8118  rexsupp  8126  mpocurryd  8213  smoel2  8297  omeu  8514  oeeui  8532  omabs  8581  omopth  8592  eldifsucnn  8594  qliftel  8741  brecop  8751  eroveu  8753  erov  8755  ecopovtrn  8761  ixpsnf1o  8880  dom2lem  8933  mapsnend  8977  xpsnen  8993  xpassen  9003  pw2f1olem  9013  xpf1o  9071  unxpdom  9163  domunfican  9226  preleqALT  9532  zfinf  9554  cantnfs  9581  brttrcl  9628  ttrclselem2  9641  tcvalg  9651  r0weon  9928  fseqenlem1  9940  acni2  9962  aceq1  10033  aceq0  10034  dfac5lem4  10042  dfac2a  10046  dfac12lem2  10061  cardcf  10168  cfeq0  10172  cfsuc  10173  cff1  10174  cfss  10181  isf32lem5  10273  fin1a2lem6  10321  zfac  10376  brdom7disj  10447  brdom6disj  10448  axrepnd  10511  axunndlem1  10512  axinfnd  10523  axacndlem5  10528  axacnd  10529  zfcndrep  10531  zfcndinf  10535  zfcndac  10536  pwfseqlem4a  10578  pwfseqlem4  10579  gruina  10735  grothomex  10746  ordpipq  10859  elnpi  10905  genpass  10926  ltprord  10947  reclem2pr  10965  reclem3pr  10966  recexpr  10968  addsrmo  10990  mulsrmo  10991  addsrpr  10992  mulsrpr  10993  ltsosr  11011  mulgt0sr  11022  supsr  11029  ltresr  11057  axpre-lttrn  11083  axpre-mulgt0  11085  prime  12604  peano5uzti  12613  rexuz  12842  ltxr  13060  qbtwnre  13145  xmulneg1  13215  supxr2  13260  ixxval  13300  fzval  13457  preduz  13598  nn0opth2  14228  hashbclem  14408  hashf1lem2  14412  eqwrd  14513  pfxeq  14652  wrd2ind  14679  cshwcsh2id  14784  eqwrds3  14917  cleq1lem  14938  rtrclreclem3  15016  rtrclreclem4  15017  relexpindlem  15019  abslt  15271  absle  15272  lenegsq  15277  abs2difabs  15291  ello12  15472  elo12  15483  o1lo1  15493  rlimuni  15506  lo1resb  15520  o1resb  15522  2clim  15528  rlimcn3  15546  climcn2  15549  addcn2  15550  mulcn2  15552  o1of2  15569  sumeq1  15645  fsum2dlem  15726  modfsummod  15751  prodeq1f  15865  prodeq1  15866  fprod2dlem  15939  nndivdvds  16224  divalg2  16368  smupval  16451  gcdval  16459  gcdass  16510  lcmval  16555  lcmass  16577  rpexp  16686  pythagtriplem2  16782  pythagtrip  16799  vdwapun  16939  0ram  16985  ramub1lem2  16992  pwsle  17450  imasleval  17499  ismre  17546  ismri  17591  iscatd2  17641  dfiso2  17733  isssc  17781  funcpropd  17863  fullpropd  17883  fthres2b  17893  fthres2c  17894  setcsect  18050  cat1lem  18057  cat1  18058  prslem  18257  drsdir  18262  posi  18277  tosso  18377  odudlatb  18485  ipoval  18490  ipolt  18495  dirge  18563  gsumpropd2lem  18641  mgmhmpropd  18660  issgrpv  18683  issgrpn0  18684  ismhm0  18752  mhmpropd  18754  mndind  18790  mgmnsgrpex  18896  issubg3  19114  isga  19260  symgfixelq  19402  psgnfval  19469  psgnval  19476  dprdw  19981  subgdmdprd  20005  isomnd  20092  isrnghm  20415  issubrg  20542  resrhm2b  20573  rngcsect  20607  rngcinv  20608  ringcsect  20641  ringcinv  20642  drngpropd  20740  orngmul  20836  islmod  20853  lmodlema  20854  lmodprop2d  20913  lsslss  20950  lbspropd  21089  lbsacsbs  21149  znleval  21547  islbs4  21825  islinds3  21827  aspval2  21891  psrbag  21910  pf1ind  22333  mdetunilem4  22593  mdetunilem9  22598  istopg  22873  basis2  22929  tg2  22943  iscld  23005  isnei  23081  isneip  23083  neiptoptop  23109  neiptopnei  23110  neitr  23158  restlp  23161  iscn  23213  cnpval  23214  iscnp  23215  regsep  23312  1stcclb  23422  2ndc1stc  23429  2ndcctbss  23433  2ndcdisj  23434  llyi  23452  nllyi  23453  hausmapdom  23478  locfinnei  23501  comppfsc  23510  elkgen  23514  txbas  23545  txcls  23582  txcnpi  23586  ptpjopn  23590  txdis1cn  23613  txtube  23618  txcmplem1  23619  hausdiag  23623  tx1stc  23628  txkgen  23630  xkococn  23638  elqtop  23675  kqreglem1  23719  elmptrab  23805  isfbas  23807  elflim2  23942  elflim  23949  hauspwpwf1  23965  alexsublem  24022  ghmcnp  24093  qustgplem  24099  tsmssubm  24121  elutop  24211  ustuqtop4  24222  isucn  24255  iscfilu  24265  ispsmet  24282  ismet  24301  isxmet  24302  ismet2  24311  imasdsf1olem  24351  blres  24409  elmopn  24420  mopni  24470  neibl  24479  nrmmetd  24552  ngppropd  24615  elcncf  24869  mulc1cncf  24885  elpi1  25025  isclmp  25077  metcld2  25287  pmltpclem1  25428  itg1climres  25694  itg2val  25708  isibl  25745  itgeq1f  25751  itgeq1fOLD  25752  itgeq1  25753  cbvitgv  25757  itgresr  25759  iblcn  25779  itgfsum  25807  dvreslem  25889  dvfsumlem2  26007  deg1ldg  26070  vieta1  26292  ulm2  26366  sincosq2sgn  26479  sincosq4sgn  26481  efopn  26638  dvdsflsumcom  27168  fsumvma2  27194  logfac2  27197  dchrptlem1  27244  lgsdchrval  27334  2lgslem1a  27371  pntibndlem3  27572  pntlemi  27584  pntleme  27588  pnt3  27592  ltsval  27628  nolt02o  27676  leltstr  27742  nocvxminlem  27763  madebday  27909  ltslpss  27917  addsprop  27985  mulsproplemcbv  28124  mulsproplem1  28125  mulsprop  28139  abslts  28258  eucliddivs  28385  bdayfinbndlem2  28477  z12sge0  28492  istrkgld  28544  istrkg2ld  28545  istrkg3ld  28546  axtgsegcon  28549  axtg5seg  28550  axtgpasch  28552  axtgupdim2  28556  legov  28670  islnopp  28824  ishpg  28844  iscgra1  28895  dfcgra2  28915  dfcgrg2  28948  brcgr  28986  brbtwn2  28991  axsegconlem1  29003  axsegcon  29013  axcontlem10  29059  edgssv2  29284  uhgr2edg  29294  isfusgrf1  29406  edgnbusgreu  29453  cplgr3v  29521  vtxdun  29568  upgr2wlk  29753  upgrtrls  29786  upgristrl  29787  upgrf1istrl  29788  dfpth2  29815  2pthnloop  29817  usgr2pth  29850  isclwlke  29863  isclwlkupgr  29864  iswwlksnx  29926  wlknewwlksn  29973  2pthon3v  30029  elwwlks2on  30047  wpthswwlks2on  30050  rusgrnumwwlkl1  30057  rusgrnumwwlkb0  30060  clwwlknp  30125  clwwlkf  30135  erclwwlknsym  30158  erclwwlkntr  30159  clwwlknonwwlknonb  30194  0trl  30210  0spth  30214  0crct  30221  0cycl  30222  upgr4cycl4dv4e  30273  upgriseupth  30295  eupth2lem2  30307  3cyclfrgrrn1  30373  4cycl2vnunb  30378  frgrncvvdeqlem2  30388  frgr2wwlk1  30417  fusgr2wsp2nb  30422  numclwlk1lem1  30457  vciOLD  30650  isvclem  30666  nmoofval  30851  isph  30911  norm3lemt  31241  isch2  31312  cmbr  31673  eigre  31924  eigorth  31927  nmopub  31997  nmfnleub  32014  cvbr  32371  mdbr  32383  dmdbr  32388  chrelat2  32459  mdsymlem2  32493  rexunirn  32579  ifeqeqx  32630  iunrnmptss  32653  fdifsupp  32776  ressupprn  32781  1stpreima  32798  fpwrelmapffslem  32823  archirng  33267  isslmd  33281  slmdlema  33282  urpropd  33310  lindflbs  33457  islbs5  33458  lindfpropd  33460  opprqus0g  33568  idlsrgval  33581  ressply1mon1p  33646  ccfldextdgrr  33835  constrsslem  33904  constrconj  33908  constrlccllem  33916  constrcbvlem  33918  dya2iocuni  34446  omsfval  34457  elcarsg  34468  itgeq12dv  34489  isrrvv  34606  reprinrn  34781  reprdifc  34790  istrkg2d  34829  axtgupdim2ALTV  34831  brafs  34835  bnj956  34938  bnj1146  34952  bnj18eq1  35088  axsepg2  35244  axsepg2ALT  35245  zltp1ne  35311  isacycgr  35346  kur14  35417  pconncn  35425  cnpconn  35431  txpconn  35433  cvmscbv  35459  cvmcov  35464  cvmsi  35466  cvmsval  35467  cvmopnlem  35479  cvmlift2lem10  35513  cvmlift3lem2  35521  cvmlift3lem6  35525  cvmlift3lem7  35526  cvmlift3lem9  35528  cvmlift3  35529  satf0op  35578  sat1el2xp  35580  satffunlem  35602  dmopab3rexdif  35606  mclsssvlem  35763  mclsind  35771  rexxfr3dALT  35840  eldm3  35962  opelco3  35976  dfon2lem6  35987  dfon2lem7  35988  dfon2lem8  35989  dfon2  35991  elfuns  36114  lemsuccf  36140  brofs  36206  5segofs  36207  brifs  36244  ifscgr  36245  brcolinear  36260  lineext  36277  brfs  36280  fscgr  36281  linecgr  36282  btwnconn1lem4  36291  btwnconn1lem8  36295  btwnconn1lem11  36298  btwnconn1lem12  36299  segcon2  36306  brsegle  36309  outsideofeq  36331  funray  36341  funline  36343  fvline  36345  linethru  36354  disjeq12dv  36416  prodeq12sdv  36419  itgeq12sdv  36420  cbvitgvw2  36449  cbvitgdavw  36482  cbvitgdavw2  36498  trer  36517  finminlem  36519  ivthALT  36536  filnetlem4  36582  axtco1  36674  axtco1from2  36676  ttcexg  36733  mh-infprim1bi  36747  knoppndvlem21  36811  bj-zfauscl  37250  bj-elgab  37265  bj-imdirvallem  37513  csboprabg  37663  topdifinffinlem  37680  icoreval  37686  isbasisrelowllem1  37688  isbasisrelowllem2  37689  relowlssretop  37696  pibp19  37747  curf  37936  ptrest  37957  poimirlem1  37959  poimirlem13  37971  poimirlem14  37972  poimirlem22  37980  poimirlem24  37982  poimirlem26  37984  poimirlem27  37985  heicant  37993  mblfinlem3  37997  mblfinlem4  37998  mbfresfi  38004  itg2addnclem3  38011  itg2addnc  38012  itg2gt0cn  38013  areacirclem5  38050  cover2  38053  cover2g  38054  fdc  38083  fdc1  38084  heibor1  38148  bfp  38162  rngosn3  38262  drngoi  38289  isdrngo1  38294  isriscg  38322  isfldidl2  38407  raldmqseu  38703  eldmxrncnvepres  38772  brressn  38869  islshpat  39480  lcvbr  39484  lshpsmreu  39572  ldual1dim  39629  cvrval  39732  cvrnbtwn3  39739  iscvlat2N  39787  ishlat3N  39817  hlrelat5N  39864  3dim0  39920  llnexatN  39984  islpln5  39998  islvol5  40042  pmapjat1  40316  ltrnu  40584  cdleme02N  40685  cdlemg33b  41170  cdlemg33c  41171  dvhb1dimN  41449  dibelval3  41610  dibopelval3  41611  dib1dim  41628  dibglbN  41629  diblsmopel  41634  dicval  41639  dicopelval  41640  dicelval3  41643  dicelval1sta  41650  dihopelvalcpre  41711  dih1dimatlem  41792  dihpN  41799  dihjatcclem4  41884  lpolsetN  41945  mapdpglem3  42138  hdmapglem7a  42390  sticksstones23  42625  exfinfldd  42659  fimgmcyclem  42995  fimgmcyc  42996  fsuppind  43040  fsuppssindlem2  43042  prjspeclsp  43062  mrefg2  43156  mzpclval  43174  eldiophb  43206  eldioph2lem1  43209  eldioph3  43215  lzenom  43219  diophin  43221  eldiophss  43223  diophrex  43224  eq0rabdioph  43225  pellexlem3  43280  elpell1qr  43296  elpell14qr  43298  elpell1234qr  43300  jm2.27  43457  rmydioph  43463  expdiophlem1  43470  expdioph  43472  pw2f1ocnv  43486  hbtlem1  43572  hbtlem7  43574  dgraalem  43594  dgraaub  43597  dflim7  43722  omabs2  43781  tfsconcatfv2  43789  tfsconcat0i  43794  nadd1suc  43841  ifpbi2  43915  inintabd  44027  cnvcnvintabd  44048  cnvintabd  44051  clcnvlem  44071  iunrelexpmin1  44156  uneqsn  44473  k0004lem2  44596  mnuprdlem1  44720  mnuprdlem2  44721  binomcxplemnotnn0  44804  2sbc6g  44863  2sbc5g  44864  iotasbc  44867  dropab1  44894  dropab2  44895  relpeq5  45396  modelaxreplem3  45428  omssaxinf2  45436  brpermmodel  45451  permaxinf2lem  45460  cbvmpo1  45549  r19.28zf  45610  disjinfi  45643  dmrelrnrel  45676  mullimc  46067  mullimcf  46074  limsuppnfd  46151  limsuppnf  46160  limsupre2  46174  limsupre2mpt  46179  limsupre3  46182  limsupre3mpt  46183  limsupre3uzlem  46184  fourierdlem42  46598  fourierdlem48  46603  fourierdlem50  46605  fourierdlem51  46606  fourierdlem54  46609  fourierdlem86  46641  ovnval2  46994  ovnsubaddlem1  47019  hoiqssbl  47074  vonicclem2  47133  f1cof1b  47540  f1ocof1ob2  47545  funressnbrafv2  47707  dfatdmfcoafv2  47717  2ffzoeq  47791  fundcmpsurbijinj  47885  ichreuopeq  47948  prproropf1olem4  47981  prprspr2  47993  prprsprreu  47994  prprreueq  47995  reuopreuprim  48001  nprmmul3  48004  isubgrgrim  48420  grtriprop  48432  isgrtri  48434  opgpgvtx  48546  pgnbgreunbgrlem1  48604  pgnbgreunbgrlem4  48610  grlimedgnedg  48622  rngcsectALTV  48766  rngcinvALTV  48767  ringcsectALTV  48800  ringcinvALTV  48801  lmod1  48983  elbigo2  49043  rrx2vlinest  49232  eloprab1st2nd  49358  i0oii  49410  io1ii  49411  lubeldm2d  49448  glbeldm2d  49449  sectpropdlem  49526  invpropdlem  49528  isopropdlem  49530  uppropd  49671  functhinc  49938  fullthinc  49940