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  1608  drsb1  2499  eleq1w  2817  eleq1d  2819  clelab  2880  rexeqfOLD  3334  rmoeq1OLD  3397  reueq1OLD  3398  rmoeq1f  3403  rabeq  3430  rabeqbidva  3432  rabeqd  3444  rabeqf  3451  cgsex4gOLD  3508  vtocl2gafOLD  3559  vtocl4gaOLD  3566  alexeqg  3630  reu2eqd  3719  sbc2or  3774  sbc5ALT  3794  rexssOLD  4036  psstr  4082  difin2  4276  r19.28z  4473  dfif6  4503  rabsneq  4620  rexreusng  4655  reurexprg  4680  rabsnifsb  4698  ssunsn2  4803  preq12bg  4829  opeq1  4849  eluni  4886  csbuni  4912  unissb  4915  iuneq12d  4997  disjxun  5117  unopab  5200  mpteq12da  5203  mpteq12f  5205  mpteq12dva  5206  dftr2c  5232  axrep1  5250  axreplem  5251  zfrepclf  5261  axsepgfromrep  5264  axsepg  5267  zfauscl  5268  reusv2lem4  5371  rabxfrd  5387  opthg  5452  otthg  5460  copsexgw  5465  copsexg  5466  opeqsng  5478  euotd  5488  elopabw  5501  pocl  5569  xpeq1  5668  elxpi  5676  vtoclr  5717  opbrop  5752  dmopab2rex  5897  resopab2  6023  dflim2  6410  dffun2  6540  fun11  6609  feq2  6686  f1eq2  6769  f1eq3  6770  foeq2  6786  brprcneu  6865  brprcneuALT  6866  ssimaexg  6964  dmfco  6974  fndmdif  7031  respreima  7055  isoeq5  7313  isoini  7330  isopolem  7337  f1oiso  7343  f1oiso2  7344  imaeqsexvOLD  7355  riotaeqdv  7361  oprabidw  7434  oprabid  7435  oprabv  7465  mpoeq123  7477  mpoeq123dva  7479  0mpo0  7488  eloprabga  7514  resoprab  7523  resoprab2  7524  elrnmpores  7543  ov  7549  ov3  7568  ov6g  7569  ovg  7570  imaeqexov  7643  caoftrn  7710  uniuni  7754  limuni3  7845  elxp4  7916  elxp5  7917  opabex3d  7962  opabex3rd  7963  opabex3  7964  releldmdifi  8042  opiota  8056  eloprabi  8060  mptmpoopabbrd  8077  mptmpoopabbrdOLD  8078  mptmpoopabbrdOLDOLD  8080  cnvf1o  8108  frxp  8123  xporderlem  8124  poxp  8125  fnwelem  8128  poxp2  8140  xpord3pred  8149  poseq  8155  soseq  8156  suppimacnv  8171  rexsupp  8179  mpocurryd  8266  smoel2  8375  omeu  8595  oeeui  8612  omabs  8661  omopth  8672  eldifsucnn  8674  qliftel  8812  brecop  8822  eroveu  8824  erov  8826  ecopovtrn  8832  ixpsnf1o  8950  dom2lem  9004  mapsnend  9048  xpsnen  9067  xpassen  9078  pw2f1olem  9088  xpf1o  9151  unxpdom  9259  domunfican  9331  preleqALT  9629  zfinf  9651  cantnfs  9678  brttrcl  9725  ttrclselem2  9738  tcvalg  9750  r0weon  10024  fseqenlem1  10036  acni2  10058  aceq1  10129  aceq0  10130  dfac5lem4  10138  dfac2a  10142  dfac12lem2  10157  cardcf  10264  cfeq0  10268  cfsuc  10269  cff1  10270  cfss  10277  isf32lem5  10369  fin1a2lem6  10417  zfac  10472  brdom7disj  10543  brdom6disj  10544  axrepnd  10606  axunndlem1  10607  axinfnd  10618  axacndlem5  10623  axacnd  10624  zfcndrep  10626  zfcndinf  10630  zfcndac  10631  pwfseqlem4a  10673  pwfseqlem4  10674  gruina  10830  grothomex  10841  ordpipq  10954  elnpi  11000  genpass  11021  ltprord  11042  reclem2pr  11060  reclem3pr  11061  recexpr  11063  addsrmo  11085  mulsrmo  11086  addsrpr  11087  mulsrpr  11088  ltsosr  11106  mulgt0sr  11117  supsr  11124  ltresr  11152  axpre-lttrn  11178  axpre-mulgt0  11180  prime  12672  peano5uzti  12681  rexuz  12912  ltxr  13129  qbtwnre  13213  xmulneg1  13283  supxr2  13328  ixxval  13368  fzval  13524  preduz  13665  nn0opth2  14288  hashbclem  14468  hashf1lem2  14472  eqwrd  14573  pfxeq  14712  wrd2ind  14739  cshwcsh2id  14845  eqwrds3  14978  cleq1lem  14999  rtrclreclem3  15077  rtrclreclem4  15078  relexpindlem  15080  abslt  15331  absle  15332  lenegsq  15337  abs2difabs  15351  ello12  15530  elo12  15541  o1lo1  15551  rlimuni  15564  lo1resb  15578  o1resb  15580  2clim  15586  rlimcn3  15604  climcn2  15607  addcn2  15608  mulcn2  15610  o1of2  15627  sumeq1  15703  fsum2dlem  15784  modfsummod  15808  prodeq1f  15920  prodeq1  15921  fprod2dlem  15994  nndivdvds  16279  divalg2  16422  smupval  16505  gcdval  16513  gcdass  16564  lcmval  16609  lcmass  16631  rpexp  16739  pythagtriplem2  16835  pythagtrip  16852  vdwapun  16992  0ram  17038  ramub1lem2  17045  pwsle  17504  imasleval  17553  ismre  17600  ismri  17641  iscatd2  17691  dfiso2  17783  isssc  17831  funcpropd  17913  fullpropd  17933  fthres2b  17943  fthres2c  17944  setcsect  18100  cat1lem  18107  cat1  18108  prslem  18307  drsdir  18312  posi  18327  tosso  18427  odudlatb  18533  ipoval  18538  ipolt  18543  dirge  18611  gsumpropd2lem  18655  mgmhmpropd  18674  issgrpv  18697  issgrpn0  18698  ismhm0  18766  mhmpropd  18768  mndind  18804  mgmnsgrpex  18907  issubg3  19125  isga  19272  symgfixelq  19412  psgnfval  19479  psgnval  19486  dprdw  19991  subgdmdprd  20015  isrnghm  20399  issubrg  20529  resrhm2b  20560  rngcsect  20594  rngcinv  20595  ringcsect  20628  ringcinv  20629  drngpropd  20727  islmod  20819  lmodlema  20820  lmodprop2d  20879  lsslss  20916  lbspropd  21055  lbsacsbs  21115  znleval  21513  islbs4  21790  islinds3  21792  aspval2  21856  psrbag  21875  pf1ind  22291  mdetunilem4  22551  mdetunilem9  22556  istopg  22831  basis2  22887  tg2  22901  iscld  22963  isnei  23039  isneip  23041  neiptoptop  23067  neiptopnei  23068  neitr  23116  restlp  23119  iscn  23171  cnpval  23172  iscnp  23173  regsep  23270  1stcclb  23380  2ndc1stc  23387  2ndcctbss  23391  2ndcdisj  23392  llyi  23410  nllyi  23411  hausmapdom  23436  locfinnei  23459  comppfsc  23468  elkgen  23472  txbas  23503  txcls  23540  txcnpi  23544  ptpjopn  23548  txdis1cn  23571  txtube  23576  txcmplem1  23577  hausdiag  23581  tx1stc  23586  txkgen  23588  xkococn  23596  elqtop  23633  kqreglem1  23677  elmptrab  23763  isfbas  23765  elflim2  23900  elflim  23907  hauspwpwf1  23923  alexsublem  23980  ghmcnp  24051  qustgplem  24057  tsmssubm  24079  elutop  24170  ustuqtop4  24181  isucn  24214  iscfilu  24224  ispsmet  24241  ismet  24260  isxmet  24261  ismet2  24270  imasdsf1olem  24310  blres  24368  elmopn  24379  mopni  24429  neibl  24438  nrmmetd  24511  ngppropd  24574  elcncf  24831  mulc1cncf  24847  elpi1  24994  isclmp  25046  metcld2  25257  pmltpclem1  25399  itg1climres  25665  itg2val  25679  isibl  25716  itgeq1f  25722  itgeq1fOLD  25723  itgeq1  25724  cbvitgv  25728  itgresr  25730  iblcn  25750  itgfsum  25778  dvreslem  25860  dvfsumlem2  25983  dvfsumlem2OLD  25984  deg1ldg  26047  vieta1  26270  ulm2  26344  sincosq2sgn  26458  sincosq4sgn  26460  efopn  26617  dvdsflsumcom  27148  fsumvma2  27175  logfac2  27178  dchrptlem1  27225  lgsdchrval  27315  2lgslem1a  27352  pntibndlem3  27553  pntlemi  27565  pntleme  27569  pnt3  27573  sltval  27609  nolt02o  27657  slelttr  27719  nocvxminlem  27739  madebday  27855  sltlpss  27862  addsprop  27926  mulsproplemcbv  28058  mulsproplem1  28059  mulsprop  28073  absslt  28190  istrkgld  28384  istrkg2ld  28385  istrkg3ld  28386  axtgsegcon  28389  axtg5seg  28390  axtgpasch  28392  axtgupdim2  28396  legov  28510  islnopp  28664  ishpg  28684  iscgra1  28735  dfcgra2  28755  dfcgrg2  28788  brcgr  28825  brbtwn2  28830  axsegconlem1  28842  axsegcon  28852  axcontlem10  28898  edgssv2  29123  uhgr2edg  29133  isfusgrf1  29245  edgnbusgreu  29292  cplgr3v  29360  vtxdun  29407  upgr2wlk  29594  upgrtrls  29627  upgristrl  29628  upgrf1istrl  29629  dfpth2  29657  2pthnloop  29659  usgr2pth  29692  isclwlke  29705  isclwlkupgr  29706  iswwlksnx  29768  wlknewwlksn  29815  2pthon3v  29871  elwwlks2on  29887  wpthswwlks2on  29889  rusgrnumwwlkl1  29896  rusgrnumwwlkb0  29899  clwwlknp  29964  clwwlkf  29974  erclwwlknsym  29997  erclwwlkntr  29998  clwwlknonwwlknonb  30033  0trl  30049  0spth  30053  0crct  30060  0cycl  30061  upgr4cycl4dv4e  30112  upgriseupth  30134  eupth2lem2  30146  3cyclfrgrrn1  30212  4cycl2vnunb  30217  frgrncvvdeqlem2  30227  frgr2wwlk1  30256  fusgr2wsp2nb  30261  numclwlk1lem1  30296  vciOLD  30488  isvclem  30504  nmoofval  30689  isph  30749  norm3lemt  31079  isch2  31150  cmbr  31511  eigre  31762  eigorth  31765  nmopub  31835  nmfnleub  31852  cvbr  32209  mdbr  32221  dmdbr  32226  chrelat2  32297  mdsymlem2  32331  rexunirn  32419  ifeqeqx  32469  iunrnmptss  32492  funcnvmpt  32591  fdifsupp  32608  ressupprn  32613  1stpreima  32630  fpwrelmapffslem  32655  isomnd  33015  archirng  33132  isslmd  33145  slmdlema  33146  urpropd  33173  orngmul  33271  lindflbs  33340  islbs5  33341  lindfpropd  33343  opprqus0g  33451  idlsrgval  33464  ressply1mon1p  33527  ccfldextdgrr  33659  constrsslem  33721  constrconj  33725  constrlccllem  33733  constrcbvlem  33735  dya2iocuni  34261  omsfval  34272  elcarsg  34283  itgeq12dv  34304  isrrvv  34421  reprinrn  34596  reprdifc  34605  istrkg2d  34644  axtgupdim2ALTV  34646  brafs  34650  bnj956  34753  bnj1146  34768  bnj18eq1  34904  axsepg2  35059  axsepg2ALT  35060  zltp1ne  35078  isacycgr  35113  kur14  35184  pconncn  35192  cnpconn  35198  txpconn  35200  cvmscbv  35226  cvmcov  35231  cvmsi  35233  cvmsval  35234  cvmopnlem  35246  cvmlift2lem10  35280  cvmlift3lem2  35288  cvmlift3lem6  35292  cvmlift3lem7  35293  cvmlift3lem9  35295  cvmlift3  35296  satf0op  35345  sat1el2xp  35347  satffunlem  35369  dmopab3rexdif  35373  mclsssvlem  35530  mclsind  35538  rexxfr3dALT  35607  eldm3  35724  opelco3  35738  dfon2lem6  35752  dfon2lem7  35753  dfon2lem8  35754  dfon2  35756  elfuns  35879  brsuccf  35905  brofs  35969  5segofs  35970  brifs  36007  ifscgr  36008  brcolinear  36023  lineext  36040  brfs  36043  fscgr  36044  linecgr  36045  btwnconn1lem4  36054  btwnconn1lem8  36058  btwnconn1lem11  36061  btwnconn1lem12  36062  segcon2  36069  brsegle  36072  outsideofeq  36094  funray  36104  funline  36106  fvline  36108  linethru  36117  disjeq12dv  36179  prodeq12sdv  36182  itgeq12sdv  36183  cbvitgvw2  36212  cbvitgdavw  36245  cbvitgdavw2  36261  trer  36280  finminlem  36282  ivthALT  36299  filnetlem4  36345  knoppndvlem21  36496  bj-zfauscl  36888  bj-elgab  36903  bj-imdirvallem  37144  csboprabg  37294  topdifinffinlem  37311  icoreval  37317  isbasisrelowllem1  37319  isbasisrelowllem2  37320  relowlssretop  37327  pibp19  37378  wl-ax11-lem8  37556  curf  37568  ptrest  37589  poimirlem1  37591  poimirlem13  37603  poimirlem14  37604  poimirlem22  37612  poimirlem24  37614  poimirlem26  37616  poimirlem27  37617  heicant  37625  mblfinlem3  37629  mblfinlem4  37630  mbfresfi  37636  itg2addnclem3  37643  itg2addnc  37644  itg2gt0cn  37645  areacirclem5  37682  cover2  37685  cover2g  37686  fdc  37715  fdc1  37716  heibor1  37780  bfp  37794  rngosn3  37894  drngoi  37921  isdrngo1  37926  isriscg  37954  isfldidl2  38039  brressn  38405  islshpat  38981  lcvbr  38985  lshpsmreu  39073  ldual1dim  39130  cvrval  39233  cvrnbtwn3  39240  iscvlat2N  39288  ishlat3N  39318  hlrelat5N  39366  3dim0  39422  llnexatN  39486  islpln5  39500  islvol5  39544  pmapjat1  39818  ltrnu  40086  cdleme02N  40187  cdlemg33b  40672  cdlemg33c  40673  dvhb1dimN  40951  dibelval3  41112  dibopelval3  41113  dib1dim  41130  dibglbN  41131  diblsmopel  41136  dicval  41141  dicopelval  41142  dicelval3  41145  dicelval1sta  41152  dihopelvalcpre  41213  dih1dimatlem  41294  dihpN  41301  dihjatcclem4  41386  lpolsetN  41447  mapdpglem3  41640  hdmapglem7a  41892  sticksstones23  42128  exfinfldd  42162  fimgmcyclem  42503  fimgmcyc  42504  fsuppind  42560  fsuppssindlem2  42562  prjspeclsp  42582  mrefg2  42677  mzpclval  42695  eldiophb  42727  eldioph2lem1  42730  eldioph3  42736  lzenom  42740  diophin  42742  eldiophss  42744  diophrex  42745  eq0rabdioph  42746  pellexlem3  42801  elpell1qr  42817  elpell14qr  42819  elpell1234qr  42821  jm2.27  42979  rmydioph  42985  expdiophlem1  42992  expdioph  42994  pw2f1ocnv  43008  hbtlem1  43094  hbtlem7  43096  dgraalem  43116  dgraaub  43119  dflim7  43244  omabs2  43303  tfsconcatfv2  43311  tfsconcat0i  43316  nadd1suc  43363  ifpbi2  43438  inintabd  43550  cnvcnvintabd  43571  cnvintabd  43574  clcnvlem  43594  iunrelexpmin1  43679  uneqsn  43996  k0004lem2  44119  mnuprdlem1  44244  mnuprdlem2  44245  binomcxplemnotnn0  44328  2sbc6g  44387  2sbc5g  44388  iotasbc  44391  dropab1  44419  dropab2  44420  relpeq5  44921  modelaxreplem3  44953  omssaxinf2  44961  brpermmodel  44976  permaxinf2lem  44985  cbvmpo1  45070  r19.28zf  45131  disjinfi  45164  dmrelrnrel  45198  mullimc  45593  mullimcf  45600  limsuppnfd  45679  limsuppnf  45688  limsupre2  45702  limsupre2mpt  45707  limsupre3  45710  limsupre3mpt  45711  limsupre3uzlem  45712  fourierdlem42  46126  fourierdlem48  46131  fourierdlem50  46133  fourierdlem51  46134  fourierdlem54  46137  fourierdlem86  46169  ovnval2  46522  ovnsubaddlem1  46547  hoiqssbl  46602  vonicclem2  46661  f1cof1b  47054  f1ocof1ob2  47059  funressnbrafv2  47221  dfatdmfcoafv2  47231  2ffzoeq  47304  fundcmpsurbijinj  47372  ichreuopeq  47435  prproropf1olem4  47468  prprspr2  47480  prprsprreu  47481  prprreueq  47482  reuopreuprim  47488  isubgrgrim  47890  grtriprop  47901  isgrtri  47903  opgpgvtx  48007  rngcsectALTV  48198  rngcinvALTV  48199  ringcsectALTV  48232  ringcinvALTV  48233  lmod1  48416  elbigo2  48480  rrx2vlinest  48669  eloprab1st2nd  48791  i0oii  48842  io1ii  48843  lubeldm2d  48880  glbeldm2d  48881  sectpropdlem  48951  invpropdlem  48953  isopropdlem  48955  functhinc  49282  fullthinc  49284