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  1607  drsb1  2498  eleq1w  2816  eleq1d  2818  clelab  2879  rexeqfOLD  3338  rmoeq1OLD  3401  reueq1OLD  3402  rmoeq1f  3407  rabeq  3434  rabeqbidva  3436  rabeqd  3448  rabeqf  3455  cgsex4gOLD  3512  vtocl2gafOLD  3563  vtocl4gaOLD  3570  alexeqg  3634  reu2eqd  3724  sbc2or  3779  sbc5ALT  3799  rexssOLD  4041  psstr  4087  difin2  4281  r19.28z  4478  dfif6  4508  rabsneq  4624  rexreusng  4659  reurexprg  4684  rabsnifsb  4702  ssunsn2  4807  preq12bg  4833  opeq1  4853  eluni  4890  csbuni  4916  unissb  4919  iuneq12d  5001  disjxun  5121  unopab  5204  mpteq12da  5207  mpteq12f  5210  mpteq12dva  5211  dftr2c  5242  axrep1  5260  axreplem  5261  zfrepclf  5271  axsepgfromrep  5274  axsepg  5277  zfauscl  5278  reusv2lem4  5381  rabxfrd  5397  opthg  5462  otthg  5470  copsexgw  5475  copsexg  5476  opeqsng  5488  euotd  5498  elopabw  5511  pocl  5580  xpeq1  5679  elxpi  5687  vtoclr  5728  opbrop  5763  dmopab2rex  5908  resopab2  6034  dflim2  6421  dffun2  6551  fun11  6620  feq2  6697  f1eq2  6780  f1eq3  6781  foeq2  6797  brprcneu  6876  brprcneuALT  6877  ssimaexg  6975  dmfco  6985  fndmdif  7042  respreima  7066  isoeq5  7323  isoini  7340  isopolem  7347  f1oiso  7353  f1oiso2  7354  imaeqsexvOLD  7365  riotaeqdv  7371  oprabidw  7444  oprabid  7445  oprabv  7475  mpoeq123  7487  mpoeq123dva  7489  0mpo0  7498  eloprabga  7524  resoprab  7533  resoprab2  7534  elrnmpores  7553  ov  7559  ov3  7578  ov6g  7579  ovg  7580  imaeqexov  7653  caoftrn  7720  uniuni  7764  limuni3  7855  elxp4  7926  elxp5  7927  opabex3d  7972  opabex3rd  7973  opabex3  7974  releldmdifi  8052  opiota  8066  eloprabi  8070  mptmpoopabbrd  8087  mptmpoopabbrdOLD  8088  mptmpoopabbrdOLDOLD  8090  cnvf1o  8118  frxp  8133  xporderlem  8134  poxp  8135  fnwelem  8138  poxp2  8150  xpord3pred  8159  poseq  8165  soseq  8166  suppimacnv  8181  rexsupp  8189  mpocurryd  8276  smoel2  8385  omeu  8605  oeeui  8622  omabs  8671  omopth  8682  eldifsucnn  8684  qliftel  8822  brecop  8832  eroveu  8834  erov  8836  ecopovtrn  8842  ixpsnf1o  8960  dom2lem  9014  mapsnend  9058  xpsnen  9077  xpassen  9088  pw2f1olem  9098  xpf1o  9161  unxpdom  9271  domunfican  9343  preleqALT  9639  zfinf  9661  cantnfs  9688  brttrcl  9735  ttrclselem2  9748  tcvalg  9760  r0weon  10034  fseqenlem1  10046  acni2  10068  aceq1  10139  aceq0  10140  dfac5lem4  10148  dfac2a  10152  dfac12lem2  10167  cardcf  10274  cfeq0  10278  cfsuc  10279  cff1  10280  cfss  10287  isf32lem5  10379  fin1a2lem6  10427  zfac  10482  brdom7disj  10553  brdom6disj  10554  axrepnd  10616  axunndlem1  10617  axinfnd  10628  axacndlem5  10633  axacnd  10634  zfcndrep  10636  zfcndinf  10640  zfcndac  10641  pwfseqlem4a  10683  pwfseqlem4  10684  gruina  10840  grothomex  10851  ordpipq  10964  elnpi  11010  genpass  11031  ltprord  11052  reclem2pr  11070  reclem3pr  11071  recexpr  11073  addsrmo  11095  mulsrmo  11096  addsrpr  11097  mulsrpr  11098  ltsosr  11116  mulgt0sr  11127  supsr  11134  ltresr  11162  axpre-lttrn  11188  axpre-mulgt0  11190  prime  12682  peano5uzti  12691  rexuz  12922  ltxr  13139  qbtwnre  13223  xmulneg1  13293  supxr2  13338  ixxval  13377  fzval  13531  preduz  13672  nn0opth2  14293  hashbclem  14473  hashf1lem2  14477  eqwrd  14577  pfxeq  14716  wrd2ind  14743  cshwcsh2id  14849  eqwrds3  14982  cleq1lem  15003  rtrclreclem3  15081  rtrclreclem4  15082  relexpindlem  15084  abslt  15335  absle  15336  lenegsq  15341  abs2difabs  15355  ello12  15534  elo12  15545  o1lo1  15555  rlimuni  15568  lo1resb  15582  o1resb  15584  2clim  15590  rlimcn3  15608  climcn2  15611  addcn2  15612  mulcn2  15614  o1of2  15631  sumeq1  15707  fsum2dlem  15788  modfsummod  15812  prodeq1f  15924  prodeq1  15925  fprod2dlem  15998  nndivdvds  16281  divalg2  16424  smupval  16507  gcdval  16515  gcdass  16566  lcmval  16611  lcmass  16633  rpexp  16741  pythagtriplem2  16837  pythagtrip  16854  vdwapun  16994  0ram  17040  ramub1lem2  17047  pwsle  17508  imasleval  17557  ismre  17604  ismri  17645  iscatd2  17695  dfiso2  17787  isssc  17835  funcpropd  17918  fullpropd  17938  fthres2b  17948  fthres2c  17949  setcsect  18105  cat1lem  18112  cat1  18113  prslem  18313  drsdir  18318  posi  18333  tosso  18433  odudlatb  18539  ipoval  18544  ipolt  18549  dirge  18617  gsumpropd2lem  18661  mgmhmpropd  18680  issgrpv  18703  issgrpn0  18704  ismhm0  18772  mhmpropd  18774  mndind  18810  mgmnsgrpex  18913  issubg3  19131  isga  19278  symgfixelq  19419  psgnfval  19486  psgnval  19493  dprdw  19998  subgdmdprd  20022  isrnghm  20409  issubrg  20539  resrhm2b  20570  rngcsect  20604  rngcinv  20605  ringcsect  20638  ringcinv  20639  drngpropd  20737  islmod  20830  lmodlema  20831  lmodprop2d  20890  lsslss  20927  lbspropd  21066  lbsacsbs  21126  znleval  21527  islbs4  21806  islinds3  21808  aspval2  21872  psrbag  21891  pf1ind  22307  mdetunilem4  22569  mdetunilem9  22574  istopg  22849  basis2  22905  tg2  22919  iscld  22981  isnei  23057  isneip  23059  neiptoptop  23085  neiptopnei  23086  neitr  23134  restlp  23137  iscn  23189  cnpval  23190  iscnp  23191  regsep  23288  1stcclb  23398  2ndc1stc  23405  2ndcctbss  23409  2ndcdisj  23410  llyi  23428  nllyi  23429  hausmapdom  23454  locfinnei  23477  comppfsc  23486  elkgen  23490  txbas  23521  txcls  23558  txcnpi  23562  ptpjopn  23566  txdis1cn  23589  txtube  23594  txcmplem1  23595  hausdiag  23599  tx1stc  23604  txkgen  23606  xkococn  23614  elqtop  23651  kqreglem1  23695  elmptrab  23781  isfbas  23783  elflim2  23918  elflim  23925  hauspwpwf1  23941  alexsublem  23998  ghmcnp  24069  qustgplem  24075  tsmssubm  24097  elutop  24188  ustuqtop4  24199  isucn  24232  iscfilu  24242  ispsmet  24259  ismet  24278  isxmet  24279  ismet2  24288  imasdsf1olem  24328  blres  24386  elmopn  24397  mopni  24449  neibl  24458  nrmmetd  24531  ngppropd  24594  elcncf  24851  mulc1cncf  24867  elpi1  25014  isclmp  25066  metcld2  25277  pmltpclem1  25419  itg1climres  25685  itg2val  25699  isibl  25736  itgeq1f  25742  itgeq1fOLD  25743  itgeq1  25744  cbvitgv  25748  itgresr  25750  iblcn  25770  itgfsum  25798  dvreslem  25880  dvfsumlem2  26003  dvfsumlem2OLD  26004  deg1ldg  26067  vieta1  26290  ulm2  26364  sincosq2sgn  26477  sincosq4sgn  26479  efopn  26636  dvdsflsumcom  27167  fsumvma2  27194  logfac2  27197  dchrptlem1  27244  lgsdchrval  27334  2lgslem1a  27371  pntibndlem3  27572  pntlemi  27584  pntleme  27588  pnt3  27592  sltval  27628  nolt02o  27676  slelttr  27738  nocvxminlem  27758  madebday  27874  sltlpss  27881  addsprop  27945  mulsproplemcbv  28077  mulsproplem1  28078  mulsprop  28092  absslt  28209  istrkgld  28403  istrkg2ld  28404  istrkg3ld  28405  axtgsegcon  28408  axtg5seg  28409  axtgpasch  28411  axtgupdim2  28415  legov  28529  islnopp  28683  ishpg  28703  iscgra1  28754  dfcgra2  28774  dfcgrg2  28807  brcgr  28845  brbtwn2  28850  axsegconlem1  28862  axsegcon  28872  axcontlem10  28918  edgssv2  29143  uhgr2edg  29153  isfusgrf1  29265  edgnbusgreu  29312  cplgr3v  29380  vtxdun  29427  upgr2wlk  29614  upgrtrls  29647  upgristrl  29648  upgrf1istrl  29649  dfpth2  29677  2pthnloop  29679  usgr2pth  29712  isclwlke  29725  isclwlkupgr  29726  iswwlksnx  29788  wlknewwlksn  29835  2pthon3v  29891  elwwlks2on  29907  wpthswwlks2on  29909  rusgrnumwwlkl1  29916  rusgrnumwwlkb0  29919  clwwlknp  29984  clwwlkf  29994  erclwwlknsym  30017  erclwwlkntr  30018  clwwlknonwwlknonb  30053  0trl  30069  0spth  30073  0crct  30080  0cycl  30081  upgr4cycl4dv4e  30132  upgriseupth  30154  eupth2lem2  30166  3cyclfrgrrn1  30232  4cycl2vnunb  30237  frgrncvvdeqlem2  30247  frgr2wwlk1  30276  fusgr2wsp2nb  30281  numclwlk1lem1  30316  vciOLD  30508  isvclem  30524  nmoofval  30709  isph  30769  norm3lemt  31099  isch2  31170  cmbr  31531  eigre  31782  eigorth  31785  nmopub  31855  nmfnleub  31872  cvbr  32229  mdbr  32241  dmdbr  32246  chrelat2  32317  mdsymlem2  32351  rexunirn  32439  ifeqeqx  32490  iunrnmptss  32513  funcnvmpt  32612  fdifsupp  32629  ressupprn  32634  1stpreima  32651  fpwrelmapffslem  32678  isomnd  33017  archirng  33134  isslmd  33147  slmdlema  33148  urpropd  33175  orngmul  33273  lindflbs  33342  islbs5  33343  lindfpropd  33345  opprqus0g  33453  idlsrgval  33466  ressply1mon1p  33528  ccfldextdgrr  33659  constrsslem  33721  constrconj  33725  constrlccllem  33733  constrcbvlem  33735  dya2iocuni  34244  omsfval  34255  elcarsg  34266  itgeq12dv  34287  isrrvv  34404  reprinrn  34592  reprdifc  34601  istrkg2d  34640  axtgupdim2ALTV  34642  brafs  34646  bnj956  34749  bnj1146  34764  bnj18eq1  34900  axsepg2  35055  axsepg2ALT  35056  zltp1ne  35074  isacycgr  35109  kur14  35180  pconncn  35188  cnpconn  35194  txpconn  35196  cvmscbv  35222  cvmcov  35227  cvmsi  35229  cvmsval  35230  cvmopnlem  35242  cvmlift2lem10  35276  cvmlift3lem2  35284  cvmlift3lem6  35288  cvmlift3lem7  35289  cvmlift3lem9  35291  cvmlift3  35292  satf0op  35341  sat1el2xp  35343  satffunlem  35365  dmopab3rexdif  35369  mclsssvlem  35526  mclsind  35534  rexxfr3dALT  35603  eldm3  35720  opelco3  35734  dfon2lem6  35748  dfon2lem7  35749  dfon2lem8  35750  dfon2  35752  elfuns  35875  brsuccf  35901  brofs  35965  5segofs  35966  brifs  36003  ifscgr  36004  brcolinear  36019  lineext  36036  brfs  36039  fscgr  36040  linecgr  36041  btwnconn1lem4  36050  btwnconn1lem8  36054  btwnconn1lem11  36057  btwnconn1lem12  36058  segcon2  36065  brsegle  36068  outsideofeq  36090  funray  36100  funline  36102  fvline  36104  linethru  36113  disjeq12dv  36175  prodeq12sdv  36178  itgeq12sdv  36179  cbvitgvw2  36208  cbvitgdavw  36241  cbvitgdavw2  36257  trer  36276  finminlem  36278  ivthALT  36295  filnetlem4  36341  knoppndvlem21  36492  bj-zfauscl  36884  bj-elgab  36899  bj-imdirvallem  37140  csboprabg  37290  topdifinffinlem  37307  icoreval  37313  isbasisrelowllem1  37315  isbasisrelowllem2  37316  relowlssretop  37323  pibp19  37374  wl-ax11-lem8  37552  curf  37564  ptrest  37585  poimirlem1  37587  poimirlem13  37599  poimirlem14  37600  poimirlem22  37608  poimirlem24  37610  poimirlem26  37612  poimirlem27  37613  heicant  37621  mblfinlem3  37625  mblfinlem4  37626  mbfresfi  37632  itg2addnclem3  37639  itg2addnc  37640  itg2gt0cn  37641  areacirclem5  37678  cover2  37681  cover2g  37682  fdc  37711  fdc1  37712  heibor1  37776  bfp  37790  rngosn3  37890  drngoi  37917  isdrngo1  37922  isriscg  37950  isfldidl2  38035  brressn  38401  islshpat  38977  lcvbr  38981  lshpsmreu  39069  ldual1dim  39126  cvrval  39229  cvrnbtwn3  39236  iscvlat2N  39284  ishlat3N  39314  hlrelat5N  39362  3dim0  39418  llnexatN  39482  islpln5  39496  islvol5  39540  pmapjat1  39814  ltrnu  40082  cdleme02N  40183  cdlemg33b  40668  cdlemg33c  40669  dvhb1dimN  40947  dibelval3  41108  dibopelval3  41109  dib1dim  41126  dibglbN  41127  diblsmopel  41132  dicval  41137  dicopelval  41138  dicelval3  41141  dicelval1sta  41148  dihopelvalcpre  41209  dih1dimatlem  41290  dihpN  41297  dihjatcclem4  41382  lpolsetN  41443  mapdpglem3  41636  hdmapglem7a  41888  sticksstones23  42129  exfinfldd  42163  fimgmcyclem  42506  fimgmcyc  42507  fsuppind  42563  fsuppssindlem2  42565  prjspeclsp  42585  mrefg2  42681  mzpclval  42699  eldiophb  42731  eldioph2lem1  42734  eldioph3  42740  lzenom  42744  diophin  42746  eldiophss  42748  diophrex  42749  eq0rabdioph  42750  pellexlem3  42805  elpell1qr  42821  elpell14qr  42823  elpell1234qr  42825  jm2.27  42983  rmydioph  42989  expdiophlem1  42996  expdioph  42998  pw2f1ocnv  43012  hbtlem1  43098  hbtlem7  43100  dgraalem  43120  dgraaub  43123  dflim7  43248  omabs2  43307  tfsconcatfv2  43315  tfsconcat0i  43320  nadd1suc  43367  ifpbi2  43442  inintabd  43554  cnvcnvintabd  43575  cnvintabd  43578  clcnvlem  43598  iunrelexpmin1  43683  uneqsn  44000  k0004lem2  44123  mnuprdlem1  44248  mnuprdlem2  44249  binomcxplemnotnn0  44332  2sbc6g  44391  2sbc5g  44392  iotasbc  44395  dropab1  44423  dropab2  44424  relpeq5  44926  modelaxreplem3  44954  omssaxinf2  44962  cbvmpo1  45060  r19.28zf  45121  disjinfi  45154  dmrelrnrel  45188  mullimc  45588  mullimcf  45595  limsuppnfd  45674  limsuppnf  45683  limsupre2  45697  limsupre2mpt  45702  limsupre3  45705  limsupre3mpt  45706  limsupre3uzlem  45707  fourierdlem42  46121  fourierdlem48  46126  fourierdlem50  46128  fourierdlem51  46129  fourierdlem54  46132  fourierdlem86  46164  ovnval2  46517  ovnsubaddlem1  46542  hoiqssbl  46597  vonicclem2  46656  f1cof1b  47047  f1ocof1ob2  47052  funressnbrafv2  47214  dfatdmfcoafv2  47224  2ffzoeq  47297  fundcmpsurbijinj  47355  ichreuopeq  47418  prproropf1olem4  47451  prprspr2  47463  prprsprreu  47464  prprreueq  47465  reuopreuprim  47471  isubgrgrim  47855  grtriprop  47866  isgrtri  47868  opgpgvtx  47968  rngcsectALTV  48149  rngcinvALTV  48150  ringcsectALTV  48183  ringcinvALTV  48184  lmod1  48367  elbigo2  48431  rrx2vlinest  48620  i0oii  48777  io1ii  48778  lubeldm2d  48815  glbeldm2d  48816  functhinc  49075  fullthinc  49077